20个Codex账户并行破解Erdős难题
Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
数学家Paul Erdős留下的第123号难题困扰学界多年，核心在于如何在互质整数幂的和中，确保选出的项互不整除。团队利用20个Codex账户并行运行，结合Lean 4和Mathlib进行了形式化证明。关键突破在于构建“齐次水平坐标系统”，将复杂的整除约束转化为同阶指数下的加法问题，并利用“内部壳层”技巧扩展了区间宽度，最终成功证明了对于任意互质三元组，所有足够大的整数均可表示为满足条件的互不整除项之和。
真正的突破在于将主要增长沿内部齐次射线展开，然后利用未使用的横向条带作为可选质量。
- 有评论者指出 AI 在数学领域的应用目标已从测试 LLM 极限的趣味练习，转变为真正解决大量数学难题并产生实际影响。
- 一位亲历者解释其撤回部分 Erdős 问题解法并非因证明错误，而是为了改进报告清晰度或完善从部分解到端到端解的过程，体现了社区审查机制的有效性。
- 针对纯数学是否“无用”的争论，有观点反驳称纯数学虽看似自指，但常意外衍生出如密码学等关键应用，且其审美价值本身即具正当性。
- 有评论者担忧随着 AI 辅助证明工具普及，年轻数学家在职业初期通过独立发现新数学获得认可的路径将变得愈发狭窄。
- 有用户质疑 AI 生成证明的可靠性，建议引入 Lean 的 comparator 工具来确保 AI 未以破坏系统健全性的方式修改 Lean 上下文。