一位数学爱好者给出的提示词，意外推动了一道可以追溯到半个多世纪前的数学难题被 ChatGPT 解出，并最终获得正式认可。

这道题出自著名的「Erdős Problems」列表中的「Erdős Problem #1196」。该列表系统整理了匈牙利数学家保罗·埃尔德什（Paul Erdős）提出的大量猜想与问题，其中许多至今仍是数学研究的前沿课题。

所谓“埃尔德什问题”，一般指围绕埃尔德什在数论、组合论、图论等领域提出的众多问题而形成的未解难题集合。埃尔德什在 20 世纪提出了极其丰富的猜想和问题，影响深远，直到今天仍有数学家持续尝试攻克。

在 Erdős Problems 官方页面上，问题 #1196 的状态目前已被标注为「PROVED（LEAN）」，并明确写明：该问题的证明已经通过定理证明辅助系统 Lean 的形式化验证。页面说明指出，这一问题与埃尔德什、András Sárközy 和 Endre Szemerédi 提出的一个猜想有关。GPT-5.4 Pro 在 Liam Price 给出的提示下，给出了对任意原始集合（primitive set）的一个上界证明。

一些海外媒体将 Price 称为“业余数学爱好者”。《Scientific American》在报道中提到，他今年 23 岁，并未接受过系统的高等数学训练。

GPT-5.4 Pro 证明了「Erdős Problem #1196」

Erdős Problem #1196 讨论的是整数集合的性质。

例如，在一个整数集合中，如果同时包含“2”和“4”，那么 4 可以被 2 整除。像这样，集合中存在“一方能整除另一方”的数对关系。

与之相对，如果从集合中任意取出两个不同的整数，都不存在“一个能整除另一个”的情况，那么这样的集合就被称为“原始集合（primitive set）”。Erdős Problem #1196 要研究的，就是对这类原始集合中某个特定求和表达式，其取值最多能大到什么程度。

据 Erdős Problems 官方页面介绍，此前数学家 Jared Duker Lichtman 已经给出了一个上界结果，而 GPT-5.4 Pro 在此基础上给出了更强的上界证明。页面上明确写道，这一成果是由「GPT-5.4 Pro（prompted by Price）」完成的。

目前，问题页面已显示为「PROVED（LEAN）」，表明该证明已经通过 Lean 的形式化验证。

Price：80 分钟“一次成型”

2026 年 4 月 14 日，Liam Price 在 X（原 Twitter）上发文称，GPT-5.4 Pro 已经解决了 Erdős Problem #1196。他在贴文中强调，这是一道长期被研究的难题，因此这一结果具有实质性意义。

在另一条贴文中，Price 进一步说明，GPT-5.4 Pro 大约用 80 分钟就“一次成型”（one-shot）地给出了完整证明，之后又花了约 30 分钟将其整理为 LaTeX 格式的数学论文。

这里的 “one-shot”，并不是指多轮试错、逐步修补，而是指在一次运行中就生成了结构完整、逻辑连贯的证明草稿。

Price 起初在 X 上表示，证明的形式化工作仍在进行中。随后，Erdős Problems 官方页面就将该问题的状态更新为「PROVED（LEAN）」。结合 Price 的公开说明与官方页面的记录，可以看出：GPT-5.4 Pro 生成的证明，经过数学界的讨论与审查，并最终通过 Lean 的形式验证，被正式记为一道未解问题的解决方案。

数学家在论坛中讨论证明细节

在 Erdős Problems 的论坛中，问题 #1196 同样被标记为「PROVED（LEAN）」。论坛里，数学家们围绕证明的思路、不同的表述方式等展开了持续讨论。

此次事件的关键在于，它并非停留在“社交媒体上有人声称 AI 解出了某题”的阶段，而是进入了更为正式的学术流程：结果被写入 Erdős Problems 官方页面，并在论坛中由数学家群体进行核查、重述和消化。

论坛讨论的重点包括：如何从概念上理解这份证明、怎样用现有的数学语言更清晰地表述、是否可以推广到相关的其他问题等。菲尔兹奖得主 Terence Tao 也在论坛中发言，就相关的随机过程和不变测度构造给出了评论。

也就是说，AI 给出的证明并不是“直接被当作正确答案照单全收”，而是先由人类数学家进行内容审阅，再进一步进入形式化验证环节。这一链条，是本次事件中非常重要的一点。

Lean 形式验证成为关键一环

这次案例中，证明通过 Lean 的形式验证同样备受关注。

Lean 是一种定理证明辅助系统，可以将数学证明用计算机可读的形式精确写出，并由程序逐步检查其逻辑是否严密、是否存在漏洞。传统的数学论文主要依靠人类审稿人阅读和推敲来判断正确性，而在 Lean 中，证明需要被拆解为更细致的逻辑步骤，由计算机进行严格检验。

在 Erdős Problems 官方页面上，关于问题 #1196 的条目明确写道：证明已经在 Lean 中通过验证。GitHub 上也公开了与该问题相关的 Lean 形式化代码。

由于生成式 AI 有时会给出“看似合理但实际上错误”的论证，因此，本次这样的流程——由 AI 提出证明草案，人类数学家进行审查，再交由 Lean 做机械化验证——被视为在数学研究中安全、可靠地使用 AI 的一个重要范式。