原创 让你更懂AI的 2025-10-24 17:37 北京
6000行代码，让GPT-5成为数学史上首位“署名作者”。
半个世纪悬而未解的数学谜题被攻克，而这次写下证明的，不只是人类。GPT-5 被正式列为论文作者之一——它写出了成千上万行可验证的数学证明代码，让一条悬赏 $1000 的 Erdős 猜想彻底落幕。
半个世纪悬而未解的数学谜题被攻克，而这次写下证明的，不只是人类。GPT-5 被正式列为论文作者之一——它写出了成千上万行可验证的数学证明代码，让一条悬赏 $1000 的 Erdős 猜想彻底落幕。
有些论文，标题看似平平，但作者行足以载入史册。
在这篇近期发布的论文中，作者包括毕业于普林斯顿大学数学系的 Boris Alexeev，以及现任俄亥俄州立大学数学系副教授的 Dustin G. Mixon——除此之外，还有两个非人类的署名：ChatGPT 与 Lean。
作者在文中写道：
“我们认为 ChatGPT 是随本文附带的形式化证明的合法作者。”
这篇论文研究的是数学家 Paul Erdős（保罗·埃尔德什） 于 1976 年提出、悬赏 1000 美元的第 707 号问题——一个与 Sidon 集和完美差集（Perfect Difference Set）有关的经典猜想 [1]。
而 GPT-5 在其中的角色远超辅助。它亲自撰写了 6000 余行 Lean 4 代码，完成了对该猜想的反例验证，并通过机器验证获得正确结论。
这是迄今为止首次有大型语言模型以正式作者身份参与并完成经机器验证的数学证明。论文作者在文中解释，随文附带的形式化证明“几乎全部由 ChatGPT 编写”，因此他们将 ChatGPT 记为该部分的作者；Lean 则作为协作系统，与之共同署名。
论文标题：
Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof
论文链接：
https://borisalexeev.com/pdf/erdos707.pdf
背景故事：悬赏$1000的数学直觉
故事要从 Erdős 说起。他一生出了数百道数学难题，其中一些附带奖金、流传数十年。第 707 号问题看似直观：
“是否每个有限 Sidon 集，都能被扩展成一个有限的完美差集（Perfect Difference Set）？”
为了让非数学背景的读者也能跟上，我们先来看看这两个名词。
Sidon 集（又称 B₂ 集）是一种“每两个元素的和都唯一”的集合。也就是说，任意两数相加（a + b 与 b + a 视为同一个），都不会得到重复的结果。例如集合 {1, 2, 4, 8} 就是一个 Sidon 集，因为它所有的两两和 (3, 5, 6, 9, 10, 12) 都各不相同。
完美差集（Perfect Difference Set, PDS）则是更极致的结构——在模 v 的意义下，它的所有非零差值恰好覆盖 1 到 v − 1 的每个数各一次。
▲ 图1. 完美差集示意：当 v = 21 时，集合 {1, 2, 5, 15, 17} 可生成 1 到 20 的全部差值，每个只出现一次。
Erdős 的直觉是：既然 Sidon 集的两两和从不重复，也许总能找到一个合适的 v，使它扩展成完美差集。如果成立，这将建立一种优雅的组合-数论桥梁。
于是他悬赏 1000 美元，希望有人证明或推翻。几十年过去，众多数学家尝试无果——直到 2025 年，GPT-5 写出了那 6000 行 Lean 代码。
反转时刻：被隐藏50年的反例
论文的结论令人意外：Erdős 错了。研究者给出了两个明确的反例，并全部通过 Lean 验证。
反例1（定理8）：当模数 （其中 为质数）时，集合 无法扩展为完美差集（Perfect Difference Set）。
反例2（定理9）：集合 在任意正模数 下均无法扩展为完美差集。
直观地说，如果把完美差集想象成一个“环形棋盘”，每个棋子代表一个数，棋子之间的跳跃差必须恰好覆盖整盘。
Erdős 认为任何 Sidon 布局都能最终摆成一个完美的圆；而作者用形式化方法证明，有些布局——比如上面这两个——无论如何都闭合不了。
更有趣的是，类似的思路其实早在 1947 年就已出现。数学家 Marshall Hall 在那年发表的论文中 [2]，无意间给出了一个等价的反例：{1,3,9,10,13}。然而他并未把这一结构上升为定理，只在文中简要提及。
本文作者指出，他们在准备过程中“进行了相当深入的文献检索，但仍未发现该结果”；甚至在对大型语言模型施加强提示（prompting）后，GPT-5 也未能检索到 Hall 的线索。
直到后续分析 Conjecture 14 时，团队才意外重新发现这一被遗忘的推理。GPT-5 与 Lean 随后对其进行了完整的形式化验证，正式确立了该反例的正确性。
技术层：AI如何写出6000行证明
这篇论文真正引发轰动的，不仅是数学结果，而是证明是怎么写出来的。
研究团队几乎不懂 Lean 语言，而 GPT-5 可以。于是他们决定让 GPT-5 全权负责形式化部分——由人类构思证明思路，GPT-5 负责生成 Lean 代码，再由 Lean 验证逻辑正确性。
流程非常清晰：
人类数学家 → GPT-5 接口 → Lean 形式化验证。
这种协作被作者称为 Vibe Coding：人和 AI 在交互中“边写边调”，像共同编程一样，直到编译器完全通过。
他们甚至创造了一个新术语——human-assisted (formal) proof，意在反转传统定义：不是“计算机辅助人类证明”，而是“人类在协助 AI 完成形式化证明”。
以下是论文第 6 节的原始定义节选：
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 秒。
作者在结语中写道：
“我们体验到的不是 computer-assisted proof，而是 human-assisted proof 。”
结语
这篇论文在数学与 AI 的交叉点提供了清晰证据：大语言模型不仅能产出“看起来合理”的文本结论，还可以在形式系统中生成可被逐步验证的证明代码。Lean 的最小可信内核保证了证明的正确性，ChatGPT 的主要贡献在于把人类用自然语言表达的思路，翻译成能够通过编译的逻辑对象。
就协作方式而言，人类给出目标与关键想法，LLM 负责形式化与调试，证明器提供正确性背书，三者形成了从问题到结论的闭环。
考虑到本次工作中形式化证明几乎全部由 ChatGPT 编写且已通过机器验证，作者给它署名具有清晰的学术根据；同时作者也建议把 Lean 作为共同署名者或与 ChatGPT 一并署名。
未来，随着更多领域将自然语言推理与形式验证打通，“AI 参与作者署名”的讨论将从个案走向常规，评价重点也会转向贡献的可验证性与可复现性。
参考文献
[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」
点击「关注」订阅我们的专栏吧
·