AI首次半自主解决厄多斯728号问题，并实现从形式化证明到高质量论文的全自动迭代，标志数学研究进入人机协同新纪元。
陶哲轩重磅发声：AI首次“半自主”攻克厄多斯难题，数学界迎来新纪元！
近日，菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩（Terence Tao）在数学社交平台 Mathstodon 上连发五条长文，详细披露了一项震撼数学界的突破性进展：人工智能工具首次在几乎无需人类干预的情况下，成功解决了一个长期悬而未决的厄多斯（Erdős）问题——编号728号问题。
更令人惊叹的是，这不仅是一次“解题”，更是一场由AI驱动的“论文创作革命”：从原始证明草稿到自然语言重写，再到逻辑漏洞修补、风格优化、文献关联，整个过程展现出前所未有的动态迭代能力。这一事件标志着AI在数学研究中的角色，已从辅助工具跃升为具备初步“科研共创”能力的智能体。
厄多斯728号问题：一个被误写的经典难题如何重获新生？
这个问题最初由数学巨人保罗·厄多斯与合作者格雷厄姆、鲁萨、施特劳斯于1975年提出，核心是探讨阶乘之间的整除关系：是否存在无穷多组整数 a, b, n，满足 a ≥ εn、b ≥ εn，并且 a!b! 能整除 n!(a+b−n)!，同时 a + b > n + C log n？乍看之下条件清晰，实则漏洞百出。
早期版本未限制 a 和 b 的上界，导致AI很快找到“技术性成立但毫无意义”的平凡解——比如令 a 极大、b 构造为 (a! / n!) − 1，虽满足整除，却完全背离原问题想探讨“中等规模组合数之间精细结构”的初衷。
几个月前，AlphaProof 团队指出这一缺陷后，社区迅速达成共识：应追加约束 a, b ≤ (1−ε)n，以排除病态构造。正是这一“问题重构”，让728号问题真正回归数学本质，也为AI的深度介入铺平道路。
ChatGPT出手：从小常数C到大常数C，AI完成关键跃迁
今年1月4日，ChatGPT 首次在修正后的约束下给出证明，但仅适用于“小常数 C”的情形。该证明随后被形式化验证工具 Aristotle 成功转译为 Lean 代码并通过机器验证。然而，团队很快发现原始论文其实早已隐含处理了小 C 情况——这意味着这次“突破”只是重复已有成果。
真正的挑战在于：能否处理“大常数 C”？这正是厄多斯等人真正关心的非平凡区域。令人意外的是，经过几轮提示工程（prompt engineering），ChatGPT 竟然成功将原论证推广至任意大的 C！尽管新证明初稿存在若干细微错误，但 Aristotle 再次展现其强大修复能力，自动补全逻辑缺口并生成可验证的 Lean 证明。
至此，AI 不仅解决了问题，还完成了从“复现”到“创新”的关键一跃。
论文写作革命：AI如何把一段Lean代码变成接近发表级的数学文章？
比解题本身更让陶哲轩兴奋的，是AI在“科学表达”层面的惊人表现。
一位参与者将 Aristotle 生成的 Lean 证明输入 ChatGPT，要求其转写为自然语言。初版输出虽生硬、缺乏文献背景、带有明显“AI腔”，但核心思路清晰可辨。经过多轮对话引导，AI 逐步优化表述，填补推理空白，最终产出一份结构完整、逻辑连贯的初稿。
更进一步，另一位研究者对 Lean 证明进行精简后，再次投入 ChatGPT 进行长达数十轮的交互式润色。结果令人震惊：新版本不仅语言流畅，还主动关联相关工作、构建叙事脉络、解释技术动机，整体质量已“接近可接受的研究论文标准”。
陶哲轩本人在厄多斯问题官网论坛亲自审阅并给予肯定评价。这种“一人提问、多人协作、AI迭代”的新型写作模式，彻底颠覆了传统学术写作“一次成稿、局部修改”的低效范式。
人机共生新范式：官方论文与AI衍生版本共存的未来图景
尽管陶哲轩仍坚持认为，核心论文的关键部分应由人类主导撰写以确保思想深度与学术品味，但他明确指出：AI在“常规证明书写”和“多版本快速生成”上的价值不可忽视。过去，学者修改论文常因怕出错而回避大幅重构；如今，借助AI+形式化验证的组合，研究者可随时生成针对不同读者（如审稿人、学生、跨领域专家）的定制化版本——有的侧重严谨性，有的强调直观解释，有的聚焦算法实现。
这些“次级文本”虽非正式出版物，却能极大提升知识传播效率。陶哲轩预言：未来一篇顶级论文或许会附带数十个AI生成的衍生版本，形成一个动态、立体的知识生态系统。这不仅是工具升级，更是科研文化的根本性变革。
技术细节揭秘：从组合恒等式到形式化验证的全链路闭环
整个突破的技术内核，其实源于一个巧妙的变量替换：令 k = a + b − n，N = a + b，则原整除条件 a!b! ∣ n!(a+b−n)! 等价于组合数恒等式 binom(N, k) ∣ binom(N, a)。AI正是在此框架下，通过分析素因子指数（Legendre 公式）构造满足条件的三元组。具体而言，当取 b = n/2，a = n/2 + O(log n) 时，可精确控制 a + b − n 落在 (C₁ log n, C₂ log n) 区间内，从而同时满足整除性与增长条件。而 Lean 的作用，就是将这一系列不等式估计与数论引理转化为机器可验的逻辑链条。
值得一提的是，Aristotle 并非简单翻译器，它能理解 ChatGPT 证明中的模糊表述，并自动寻找缺失的中间引理或反例检验边界情况——这种“理解-修复-验证”闭环，才是此次突破的技术基石。
为什么这件事值得所有科研工作者关注？
这不仅是数学圈的内部新闻，更是整个科研范式的预警信号。AI 此次展示的能力——理解模糊问题、重构合理假设、生成原创证明、多轮优化表达、与形式化系统联动——已覆盖科研流程的核心环节。对于工程师、生物学家、经济学家而言，这意味着未来你只需描述一个模糊的研究目标，AI 就能帮你梳理文献、设计实验、分析数据、撰写初稿，甚至预判审稿人质疑。
陶哲轩所描绘的“高频率、多版本、动态演化的知识表达”模式，将极大降低科研沟通成本，加速跨学科融合。当然，人类的角色不会消失，而是转向更高维的“问题定义者”与“意义赋予者”——正如陶哲轩所说：“我们仍需那篇‘官方’论文，但它的诞生方式，已经永远改变。”