GPT Astra 协作攻克 Erdős #357:Lean 验证首次突破 1986 年 3/2 下界
kevrussell · x · 2026-11-03
Kevin Russell 与 GPT Astra 合作,为 Erdős 问题 #357 的任意顺序版本给出一个候选小步推进:当 k ≥ 10²² 时,k 个不同整数若所有连续段和互不相同,所需的最大数上界需超过 (3/2 + 10⁻¹⁰)k,超越了 Hegyvári 1986 年的 3/2 界。要点:
- 问题定义:从 1..N 中选 k 个不同数排成一列,要求所有相邻连续段之和两两不同,求最小 N(即 OEIS A364153);k=19 时 N=29 由计算机搜索得出。
- 论证由 GPT Astra 协作写出,并给出 Lean 形式化证明,Lean 逐行验证通过;Ford 的审计未发现漏洞,证明材料与审计记录已在 GitHub 开源。
- 作者明确说明:目前所有审查均为 AI 完成,尚无人类专家评审,欢迎专家检验;收益本身很小且只在极大的 k 下成立。
所属事件:GPT Astra 辅助 Erdős 问题 #357 取得下界新进展(3 条相关)→
「研究」频道最新
- 3D World Simulator：联合预测外观几何触觉，50Hz 交互式世界模拟 — XRarchitect · 2026-11-03
- 权重空间编程结果获独立复现，最新模型出现阶跃新能力 — basedjensen · 2026-11-03
- ARC Prize 2026 收官：1.85 万人参赛提交 6.7 万次，12 月 4 日揭晓 — GregKamradt · 2026-11-03
- 心脏 MRI 的 AI 读片能否先于临床医生？Lancet 子刊研究给出答案 — EricTopol · 2026-11-03
- 「涌现能力」宣称遭质疑；Fleet 拟雇人教 AI 做机制可解释性研究 — sebkrier · 2026-11-03
- Goodfire 推出神经几何研究系列：用流形理解并控制大模型内部 — burny_tech · 2026-11-03