原创 让你更懂AI的 2025-10-24 17:37 北京
6000行代码，让GPT-5成为数学史上首位“署名作者”。
半个世纪悬而未解的数学谜题被攻克，而这次写下证明的，不只是人类。GPT-5 被正式列为论文作者之一——它写出了成千上万行可验证的数学证明代码，让一条悬赏 $1000 的 Erdős 猜想彻底落幕。
✨ **AI驱动的数学突破：** GPT-5 成功解决了困扰数学界半个世纪的 Erdős 猜想（第 707 号问题），该猜想涉及 Sidon 集和完美差集。GPT-5 编写了超过 6000 行的 Lean 4 代码，完成了对猜想反例的机器验证，这是 AI 首次作为正式作者参与并完成数学证明。
🤝 **AI与人类的创新协作模式：** 本次研究开创了“人类协助 AI 完成形式化证明”（human-assisted proof）的新模式。人类数学家负责构思证明思路，GPT-5 负责生成并调试 Lean 代码，Lean 验证器则确保逻辑的严谨性。这种 Vibe Coding 的交互方式，实现了高效的科研协作。
💡 **对数学猜想的颠覆性结论：** 论文的结论推翻了 Erdős 的直觉，提供了两个明确的反例，证明了并非所有有限 Sidon 集都能扩展为完美差集。其中一个反例早在 1947 年就已由数学家 Marshall Hall 提出，但未被深入研究，GPT-5 的验证使其正式确立。
🚀 **AI作者署名的学术意义：** 由于 GPT-5 贡献了几乎全部的形式化证明代码并获得了机器验证，作者将其列为论文作者具有充分的学术依据。这为未来 AI 在科研领域的贡献提供了新的署名模式，评价重点将转向贡献的可验证性与可复现性。
原创 让你更懂AI的 2025-10-24 17:37 北京
6000行代码，让GPT-5成为数学史上首位“署名作者”。
import Mathlib
/-- A Sidon set ‘A‘ is a setwhere all pairwise sums ‘i + j‘ are unique,
up to swapping the addends. -/
def IsSidon {α : Type*} [AddCommMonoid α] (A : Set α) : Prop :=
∀ {|i1 i2 j1 j2 : α|}, i1 ∈ A → i2 ∈ A → j1 ∈ A → j2 ∈ A →
i1 + i2 = j1 + j2 →
(i1 = j1 ∧ i2 = j2) ∨ (i1 = j2 ∧ i2 = j1)
/-- ‘B‘ is a perfect difference set modulo ‘v‘ if there is a bijection between
non-zero residues mod ‘v‘ and distinct differences ‘a - b‘, where ‘a, b ∈ B‘. -/
def IsPerfectDifferenceSetModulo (B : Set Z) (v : N) : Prop :=
B.offDiag.BijOn (fun (a, b) => (a - b : ZMod v)) {x : ZMod v | x ̸= 0}
/--
**Erd\H{o}s problem 707**:
Any finite Sidon set of natural numbers can be embedded in a perfect difference
set modulo ‘v‘ for some ‘v ̸= 0‘.
-/
def erdos_707 : Prop :=
∀ A : Set N, A.Finite → IsSidon A →
∃ (B : Set Z) (v : N),
v ̸= 0 ∧
(↑) ’’ A ⊆ B ∧
IsPerfectDifferenceSetModulo B v
/--
The Sidon set {1, 2, 4, 8, 13} does not extend to a perfect difference set
modulo v for any nonnegative v.
-/
theorem not_erdos_707AM : ¬ erdos_707 :=
not_erdos_707_given_counterexample
counterexampleAM
counterexampleAM_finite
counterexampleAM_Sidon
counterexampleAM_noExt这些定义看似简短，却是整个形式化体系的骨架。IsSidon 和 IsPerfectDifferenceSetModulo 分别刻画了“和唯一性”和“差覆盖”的数学条件；erdos_707 抽象化地表达了 Erdős 猜想的命题，而 not_erdos_707AM 则是它的形式化否定。GPT-5 不仅能生成这些定义，还能在交互中不断修正语法与逻辑错误。论文特别指出，GPT-5 会自动检测到 Lean 编译器报错并尝试自我修复——这种“能编译即正确”的特性，让 Lean 成为验证 AI 生成推理最理想的语言之一。此外，作者在生成命题时还专门核对了与人类数学表述的一致性：防止把 v = 0 的“无限情形”混入推理中——这种细微错误曾出现在 DeepMind 的 Formal Conjectures 数据集中，一旦出现就会导致命题方向相反。最终，GPT-5 写出了超过 6000 行 Lean 4 代码，其中包含 26 个定义、169 个引理和 4 个主要定理，在普通笔记本上编译验证仅需不到 30 秒。作者在结语中写道：结语
参考文献
[1] Paul Erdős. Problems and Results in Additive Number Theory. Collected Papers of Paul Erdős, Vol. 3.
[2] Marshall Hall Jr. Combinatorial Analysis and Finite Projective Planes. Transactions of the American Mathematical Society, 1947.
[3] Lean Community & mathlib Team. The Lean Theorem Prover and mathlib Library. https://leanprover-community.github.io/
更多阅读#投 稿 通 道# 让你的文字被更多人看到 如何才能让更多的优质内容以更短路径到达读者群体，缩短读者寻找优质内容的成本呢？答案就是：你不认识的人。总有一些你不认识的人，知道你想知道的东西。PaperWeekly 或许可以成为一座桥梁，促使不同背景、不同方向的学者和学术灵感相互碰撞，迸发出更多的可能性。 PaperWeekly 鼓励高校实验室或个人，在我们的平台上分享各类优质内容，可以是最新论文解读，也可以是学术热点剖析、科研心得或竞赛经验讲解等。我们的目的只有一个，让知识真正流动起来。📝 稿件基本要求：• 文章确系个人原创作品，未曾在公开渠道发表，如为其他平台已发表或待发表的文章，请明确标注 • 稿件建议以 markdown 格式撰写，文中配图以附件形式发送，要求图片清晰，无版权问题• PaperWeekly 尊重原作者署名权，并将为每篇被采纳的原创首发稿件，提供业内具有竞争力稿酬，具体依据文章阅读量和文章质量阶梯制结算📬 投稿通道：• 投稿邮箱：hr@paperweekly.site • 来稿请备注即时联系方式（微信），以便我们在稿件选用的第一时间联系作者• 您也可以直接添加小编微信（pwbot02）快速投稿，备注：姓名-投稿△长按添加PaperWeekly小编🔍现在，在「知乎」也能找到我们了进入知乎首页搜索「PaperWeekly」点击「关注」订阅我们的专栏吧·AI辅助创作，多种专业模板，深度分析，高质量内容生成。从观点提取到深度思考，FishAI为您提供全方位的创作支持。新版本引入自定义参数，让您的创作更加个性化和精准。
鱼阅，AI 时代的下一个智能信息助手，助你摆脱信息焦虑