Claude 在 Lean 中形式化了费马大定理

Anthropic 最近完成了一项大规模的研究任务。一个内部模型工作了 11 天，使用 Lean 4 证明语言将费马大定理进行了形式化。

这并不是一项新的数学发现。安德鲁·怀尔斯（Andrew Wiles）在 1995 年就证明了这个定理。Anthropic 所做的是将现有的证明转化为代码。这使得计算机能够以绝对的确定性检查每一个逻辑步骤。

该项目的规模非常庞大： • 该模型生成了 1300 万行 Lean 代码。 • 它证明了 30,300 个中间定理。 • 它使用了近 60 亿个输出 token。

该模型大部分时间都在自主运行。人类仅偶尔提供高层级的指导。该过程在深夜无人看管时完成，系统自动记录了这一成功结果。

两点需要注意：

  1. 该模型是一个内部研究工具。你目前还无法通过 API 访问它。它与你今天使用的 Claude 模型不同。
  2. 对开发者的真正价值在于名为 Prove2Me 的协调层。

Prove2Me 是一个开源工具。它使用依赖图来管理任务。它不是一个简单的检查清单，而是创建了一张证明之间如何相互关联的地图。

这种结构解决了智能体（agent）工作流中的两个主要问题：

  • 它防止多个智能体重复进行相同的工作。
  • 它为智能体提供了共享记忆，使它们不会忘记主要目标。

大多数智能体工作流失败的原因是随着时间的推移会丢失上下文。使用共享的外部图谱而不是长对话窗口，可以使任务保持在正轨上。

如果你构建智能体工作流，你应该研究 Prove2Me 的架构。即使你不使用 Anthropic 的研究模型，它们协调任务的方式也是进行长程任务（long horizon work）的蓝图。

Source: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36

Optional learning community: https://t.me/GyaanSetuAi