MAP：数学自动化形式化项目
AI已能自动形式化费马大定理（1300万行代码），我们正站在将所有已知数学转化为机器可验证代码的临界点，MAP项目将绘制全人类数学版图。
我们即将把所有已知数学转化为形式化代码。
这相当于数学界的人类基因组计划，或是当代的AlphaFold。
9月4日，Anthropic通过形式化费马大定理震惊了数学界。
费马于1637年著名地提出了这一定理，安德鲁·怀尔斯爵士与理查德·泰勒于1995年证明了它，而最近凯文·巴扎德启动了一个项目来将其形式化：将人类证明转化为机器代码。长期以来，这被视为白日梦，而巴扎德获得了90万英镑的资助，计划用5年时间完成。即便如此，这也只是触及表面，因为费马证明还依赖于20世纪大量的数学文献。
因此，当Claude仅用11天就写出1300万行代码，自动形式化了费马证明及其所有前置文献时，这令人震惊不已。对巴扎德而言，这如今为他打开了形式化朗兰兹纲领文献的机会，他担心其中可能存在细微错误。这一成就若放在去年还会被视为疯狂之举，但实际上其影响深远得多。
我们现在有机会形式化人类目前已知的所有数学。正如AlphaFold整理了人类已知的2亿种蛋白质，MAP项目旨在数学领域实现同等壮举：为所有已知数学创建全面的形式化数据库。与其他科学领域困扰的复制危机不同，形式化过程能够标记文献中的错误，这些错误在历史上偶尔会动摇整个研究计划的基础。我们已经在近期AI用于数学的结果中看到了这方面的早期案例。
Claude的成就不仅仅是一个孤立的数据点，而是一个不断增长序列中的一环。早在Deepmind的IMO银牌仍占据巅峰之时，自动形式化数学的记录大约为400行代码。
- 2025年6月，随着de Bruijn的ABC定理的形式化完成，记录跃升至3.5K行代码。
- 2025年9月，在人类辅助下对素数定理的自动形式化突破了25K行代码，完成了Terry Tao和Alex Kontorovich在2024年设定的挑战。
- 2026年3月，Maryna Viazovska关于球堆积的菲尔兹奖工作的自动形式化总计达200K行代码。
- 2026年6月，OpenAI对Erdős单位距离猜想的自动形式化跨越了1M行代码的门槛。
- 如今，Claude对费马大定理的证明达到了13M行代码，标志着五个数量级增长中的平滑指数趋势。
尽管费马大定理证明的规模令人震惊，但在对数坐标图上，这一趋势变得更加清晰可见：
除了原始代码长度之外，费马大定理的证明还汲取了现代数学中极为广阔的领域。AI代理所展现的数学内容复杂性和自主水平的不断提升，实在令人叹为观止。
我的数学生涯始于数论。2019年，我来到牛津大学攻读博士学位，师从James Maynard，深受素数之谜的吸引。然而，也正是在那一年，Kevin Buzzard在牛津研讨会上作了一场关于一种名为Lean的新编程语言的报告：
他的演讲重塑了我的神经末梢。
他阐述了如何将自然语言数学转化为Lean语言，从而将证明的正确性转化为程序的编译过程。Buzzard本人，在听了Tom Hales关于开普勒猜想历史性形式化的2017年演讲后，“沉迷于”Lean编程。开普勒猜想本身是一个数百年未解的问题，其最终解决方案之复杂，以至于人类审稿人无法确切验证。但经过十多年的努力，开普勒猜想终于被形式化。
Buzzard的演讲立刻让我信服了机器验证的力量，而Lean能够处理的日益复杂的数学主题，则给人一种不可避免的感觉。正如他所说，这是一场真正的“数学数字化”革命。
与此同时，我知道在人工智能领域，继ImageNet、AlphaZero和Transformer之后，一场平行的革命正在酝酿。如今，聊天机器人的兴起——以及过去一年智能体的发展——已将这场AI革命推向了前所未有的高度。
直到最近，我的工作仍专注于数论，只是远远地关注着AI和形式化的发展。手动编程本身就是一项专业技能，即便是专家，在翻译即使是自然语言数学的小片段时也需耗费大量精力。
但就在过去一年，我发现自己站在了数学史上一个独特时刻的前线。AI与形式化的革命正汇聚成一种混合体：自动形式化。AI智能体自主进行形式化的能力正在飞速提升，无论是生成代码的数量还是质量都在不断提高。
早年我在远处观望AI与形式化进展时，注意到大多数同行不仅对进展速度不屑一顾，对其在该领域将产生的影响也嗤之以鼻。我保持沉默，但始终觉得这种轻视令人费解。然而，过去一年AI在数学与形式化方面无可否认的进步，印证了我对该领域发展轨迹的预测。直到今年，我才意识到自己拥有发声的机会，虽带有些许矛盾心理，却能提供澄清视角。在当前数学转型之际，面对感知中的困惑与混乱，此类声音比以往任何时候都更为必要。
AI如今已能形式化研究生数学课程中的教学内容，涵盖代数、分析、几何、拓扑及应用数学的核心主题；进而延伸至所有教科书乃至更广泛的研究文献。由于数学本质上是累积性的，MAP将代表一项历史性努力，旨在绘制全人类数学已知领域的版图。
粗略估计，整个数学语料库的规模约为100亿行代码，这是基于Claude当前效率水平的估算（更不用说未来的效率提升了）。如今，在学术界、前沿实验室、慈善机构及政府间的充分协调与资金支持下，我们有望在明年实现这一目标。
随着事态迅速发展，回应时机有限，更多细节将陆续公布。衷心感谢@patshafto对DARPA expMath项目的领导，以及@ericweinstien在MAP开发中提供的建议。
除验证本身的内在价值外，MAP还将成为未来数学的基石。它作为关键基础设施，将支撑下一代研究的发展。
因此，MAP有望为未来的发现奠定基础。在众多引人注目的AI生成数学成果中，这些证明本身似乎缺乏真正的原创性：那些（客观上令人瞩目的）结果利用了已知方法的巧妙组合。当前关于AI用于数学的许多评论假设这种情况将永远持续，且AI将始终缺乏新颖见解。然而，完全显式的代码有望为下一代模型提供精确的训练场。
因此，我们现在将绘制这一领域的版图，并提供一个坚实的基础，以便随后出发探索数学的前沿。
