新版：Aleph Prover 已形式化验证 OpenAI 对 Paul Erdős 平面单位问题的反证。我们以开源形式发布该形式化结果，以便其他研究者检查、扩展并独立验证此结论。详见此处：https://logicalintelligence.com/blog/aleph-prover-erdos-disproof-lean-4-formal-methods…

Aleph Prover 使用形式化方法反证 Erdős 定理

来源：https://logicalintelligence.com/blog/aleph-prover-erdos-disproof-lean-4-formal-methods Aleph Prover

形式化平面

单位问题反证

Aleph Prover

形式化平面

单位问题反证

上周，OpenAI 展示了人工智能系统能够帮助发现新的数学方法，其最新反例针对 Paul Erdős 的一个猜想，相关公告详见 https://x.com/OpenAI/status/2057176201782075690。我们 Logical Intelligence（https://logicalintelligence.com/）将此视为挑战，并使用最新版 Aleph Prover 智能体系统在 Lean 4 中对该结果进行了形式化验证。Aleph Prover 已形式化（http://github.com/logical-intelligence/erdos-unit-distance）了平面单位问题的反证，效仿近期 OpenAI 使用 AI 寻找 Paul Erdős 猜想反例的成果。

该结果现已成为 Lean 4 中可由机器检查的产物。

这为数学和计算机科学等不同领域的研究指明了新方向：AI 能够显著加速研究进展。这不仅在于证明定理，同样重要的是发现反例（因为研究者同样在此投入大量时间），从而让研究进展大幅提速。

之所以重要，是因为复杂的数学结果依赖于包含众多中间引理的大型证明结构。形式化使我们能够以程序化的方式验证这些结果，减少专家需要人工检查的证明表面积，并在未来工作中复用已验证的组件。

对于 AI 研究而言，这可将一项艰难的数学发现转化为经过验证的证明数据，供模型学习，并让未来系统在此基础上构建。

方向已然明确。AI 系统能够生成候选证明与程序，而形式化方法则可大规模验证它们或构建反例。Aleph Prover 负责生成形式化证明结构，Lean 4 作为可信验证器。这确保了正确性是完全确定性的，且无需信任 AI 系统。这是可验证 AI 以及下一代形式化验证代码生成的基础。

上周，OpenAI 展示了人工智能系统能够帮助发现新的数学方法，其最新反例针对 Paul Erdős 的一个猜想，相关公告详见 https://x.com/OpenAI/status/2057176201782075690。我们 Logical Intelligence（https://logicalintelligence.com/）将此视为挑战，并使用最新版 Aleph Prover 智能体系统在 Lean 4 中对该结果进行了形式化验证。Aleph Prover 已形式化（http://github.com/logical-intelligence/erdos-unit-distance）了平面单位问题的反证，效仿近期 OpenAI 使用 AI 寻找 Paul Erdős 猜想反例的成果。

该结果现已成为 Lean 4 中可由机器检查的产物。

这为数学和计算机科学等不同领域的研究指明了新方向：AI 能够显著加速研究进展。这不仅在于证明定理，同样重要的是发现反例（因为研究者同样在此投入大量时间），从而让研究进展大幅提速。

之所以重要，是因为复杂的数学结果依赖于包含众多中间引理的大型证明结构。形式化使我们能够以程序化的方式验证这些结果，减少专家需要人工检查的证明表面积，并在未来工作中复用已验证的组件。

对于 AI 研究而言，这可将一项艰难的数学发现转化为经过验证的证明数据，供模型学习，并让未来系统在此基础上构建。

方向已然明确。AI 系统能够生成候选证明与程序，而形式化方法则可大规模验证它们或构建反例。Aleph Prover 负责生成形式化证明结构，Lean 4 作为可信验证器。这确保了正确性是完全确定性的，且无需信任 AI 系统。这是可验证 AI 以及下一代形式化验证代码生成的基础。

动机

我们近期发布了关于 Aleph Prover 在顶级形式推理基准测试（https://logicalintelligence.com/blog/aleph-prover-tops-leading-benchmarks）中取得领先成果的文章。Aleph Prover 是我们自研的证明智能体。

构建 Aleph Prover 的目标是以更大规模、更快速度、更低成本以及更强验证保障来求解并形式化日益复杂的问题。

基准测试工作帮助我们识别了前版 Aleph Prover 的局限。过去数月，我们一直在开发新版本，旨在处理更复杂的证明搜索与形式化任务。

OpenAI 近期关于平面单位距离猜想的成果（https://x.com/OpenAI/status/2057176201782075690）为形式化验证提出了极具挑战性的难题。该证明涉及复杂的数学依赖链，正是我们为下一代 Aleph Prover 设计的长程形式化问题类型。前版 Aleph Prover 无法形式化该结果，因此成为我们最新迭代的理想基准测试。新系统成功将其转化为可由机器检查的证明，进一步确认我们正朝着可验证 AI 的正确方向迈进。

动机

我们近期发布了关于 Aleph Prover 在顶级形式推理基准测试（https://logicalintelligence.com/blog/aleph-prover-tops-leading-benchmarks）中取得领先成果的文章。Aleph Prover 是我们自研的证明智能体。

构建 Aleph Prover 的目标是以更大规模、更快速度、更低成本以及更强验证保障来求解并形式化日益复杂的问题。

基准测试工作帮助我们识别了前版 Aleph Prover 的局限。过去数月，我们一直在开发新版本，旨在处理更复杂的证明搜索与形式化任务。

OpenAI 近期关于平面单位距离猜想的成果（https://x.com/OpenAI/status/2057176201782075690）为形式化验证提出了极具挑战性的难题。该证明涉及复杂的数学依赖链，正是我们为下一代 Aleph Prover 设计的长程形式化问题类型。前版 Aleph Prover 无法形式化该结果，因此成为我们最新迭代的理想基准测试。新系统成功将其转化为可由机器检查的证明，进一步确认我们正朝着可验证 AI 的正确方向迈进。

该过程需要整合 252 个 Mathlib 模块。我们的形式化工作运用了广泛的数学工具：解析素数估计、类域塔、pro-p 伽罗瓦群、Golod-Shafarevich 方法、连续群上同调，并辅以测度论格点计数与欧几里得几何。

那么，一个 33,087 行的证明究竟长什么样？

该过程需要整合 252 个 Mathlib 模块。我们的形式化工作运用了广泛的数学工具：解析素数估计、类域塔、pro-p 伽罗瓦群、Golod-Shafarevich 方法、连续群上同调，并辅以测度论格点计数与欧几里得几何。

那么，一个 33,087 行的证明究竟长什么样？

当前的形式化结果依赖于 2 个来自教科书的外部定理（详见附录）。这些结果尚未在 Mathlib 中实现，因此我们在此版本的证明中将其视为可信假设。初始阶段我们有约 30 个此类依赖，最终将其缩减至 2 个。

当前的形式化结果依赖于 2 个来自教科书的外部定理（详见附录）。这些结果尚未在 Mathlib 中实现，因此我们在此版本的证明中将其视为可信假设。初始阶段我们有约 30 个此类依赖，最终将其缩减至 2 个。

人机协同与验证

我们首先运行了一轮 Aleph Prover，随后由人工审阅证明的一小部分，接着进行第二轮 Aleph Prover 运行，最终产出结果。感谢所有参与审阅的人员！

如您所知，LLM 有时会产生幻觉并输出无意义内容，有时甚至会故意试图欺骗检查器，生成看似正确实则不然的内容。

在 Lean 4 的情况下，大部分问题可通过编译器、检查器和比较器进行校验。这使我们能够在无人介入的情况下运行多轮代码改进迭代。

Lean 4 无法验证的是那些尚未形式化的经典定理的外部引用。鉴于目前仅有小部分数学内容在 Lean 中完成了形式化，要形式化 OpenAI 证明中使用的每个经典定理仍是一项艰巨任务。

Aleph Prover 的最终输出在其证明中依赖于两个此类外部结果。因此，我们需要检查三项内容：

1. 问题陈述本身是否从英语正确翻译为 Lean 4。
2. 两个外部定理在 Lean 4 中的表述是否与标准教科书中完全一致。
3. 证明器是否以某种方式骗过了我们或 Lean 4 内核。

我们借助专业数学家检查了前两点。感谢我们的外部审阅者 Sergey Galkin（https://scholar.google.com/citations?user=-aLTImcAAAAJ）、Mark Obozov（https://github.com/krammnic）、Browning, Thomas L（http://math.berkeley.edu/~tb65536）、Kevin Buzzard（https://profiles.imperial.ac.uk/k.buzzard）、Johan Commelin（https://math.commelin.net/），以及我们的内部数学家团队：Michael Freedman（https://dblp.org/pid/f/MichaelHFreedman.html）、Michael Mulligan（https://scholar.google.com/citations?user=IZZSYUAAAAAJ&hl=en）和 Milo Moses（https://milomoses.info/）。特别感谢 Kevin Buzzard，他在 Aleph Prover 第一轮工作后发现外部定理表述中存在错误，并提供了反馈，使 Aleph Prover 能在第二轮中进行修正。

我们通过构建项目并运行比较器工具来检查第三点，该工具使用两个独立的 Lean 内核重新验证证明，并确保其与所陈述的定理一致，且不包含隐藏的公理。

我们以开源形式发布该形式化结果，以便其他研究者检查、扩展并独立验证此结论。

部分外部定理已在仓库 https://github.com/AlexKontorovich/PrimeNumberTheoremAnd 中完成形式化。Aleph Prover 自行发现该仓库并建议复用这些形式化成果。我们感谢 Alex Kontorovich（https://sites.math.rutgers.edu/~alexk/）以及该项目的广大数学界贡献者。

人机协同

与验证

我们首先运行了一轮 Aleph Prover，随后由人工审阅证明的一小部分，接着进行第二轮 Aleph Prover 运行，最终产出结果。感谢所有参与审阅的人员！

如您所知，LLM 有时会产生幻觉并输出无意义内容，有时甚至会故意试图欺骗检查器，生成看似正确实则不然的内容。

在 Lean 4 的情况下，大部分问题可通过编译器、检查器和比较器进行校验。这使我们能够在无人介入的情况下运行多轮代码改进迭代。

Lean 4 无法验证的是那些尚未形式化的经典定理的外部引用。鉴于目前仅有小部分数学内容在 Lean 中完成了形式化，要形式化 OpenAI 证明中使用的每个经典定理仍是一项艰巨任务。

Aleph Prover 的最终输出在其证明中依赖于两个此类外部结果。因此，我们需要检查三项内容：

1. 问题陈述本身是否从英语正确翻译为 Lean 4。
2. 两个外部定理在 Lean 4 中的表述是否与标准教科书中完全一致。
3. 证明器是否以某种方式骗过了我们或 Lean 4 内核。

我们借助专业数学家检查了前两点。感谢我们的外部审阅者 Sergey Galkin（https://scholar.google.com/citations?user=-aLTImcAAAAJ）、Mark Obozov（https://github.com/krammnic）、Browning, Thomas L（http://math.berkeley.edu/~tb65536）、Kevin Buzzard（https://profiles.imperial.ac.uk/k.buzzard）、Johan Commelin（https://math.commelin.net/），以及我们的内部数学家团队：Michael Freedman（https://dblp.org/pid/f/MichaelHFreedman.html）、Michael Mulligan（https://scholar.google.com/citations?user=IZZSYUAAAAAJ&hl=en）和 Milo Moses（https://milomoses.info/）。特别感谢 Kevin Buzzard，他在 Aleph Prover 第一轮工作后发现外部定理表述中存在错误，并提供了反馈，使 Aleph Prover 能在第二轮中进行修正。

我们通过构建项目并运行比较器工具来检查第三点，该工具使用两个独立的 Lean 内核重新验证证明，并确保其与所陈述的定理一致，且不包含隐藏的公理。

我们以开源形式发布该形式化结果，以便其他研究者检查、扩展并独立验证此结论。

部分外部定理已在仓库 https://github.com/AlexKontorovich/PrimeNumberTheoremAnd 中完成形式化。Aleph Prover 自行发现该仓库并建议复用这些形式化成果。我们感谢 Alex Kontorovich（https://sites.math.rutgers.edu/~alexk/）以及该项目的广大数学界贡献者。

下一步计划？

该问题提升了 AI 辅助形式化的标杆，而新版本 Aleph Prover 成功应对了挑战。

不应将本次形式化误解为完全自主数学推理的证据。相反，它表明 AI 辅助的定理形式化能够以过去无法实现的方式规模化推广。

OpenAI 证明了 AI 系统确实能够帮助发现新数学。像 Aleph Prover 这样的形式化验证系统则可将这些发现转化为可复用、可机器检查的基础设施，为 AI 建立新的验证层。

下一步计划？

该问题提升了 AI 辅助形式化的标杆，而新版本 Aleph Prover 成功应对了挑战。

不应将本次形式化误解为完全自主数学推理的证据。相反，它表明 AI 辅助的定理形式化能够以过去无法实现的方式规模化推广。

OpenAI 证明了 AI 系统确实能够帮助发现新数学。像 Aleph Prover 这样的形式化验证系统则可将这些发现转化为可复用、可机器检查的基础设施，为 AI 建立新的验证层。

附录

Aleph Prover 未形式化 OpenAI 证明中使用的两个经典定理。结果陈述如下。

Golod-Shafarevich 不等式（1964）：对于每个素数 p 和每个非平凡有限 p-群 Q，存在不等式

d(Q)^2 < 4 r(Q)

其中 d(Q) 是生成元秩，定义为 Q 的最小生成集大小；r(Q) 是关系秩，定义为