让AI理解费马大定理的证明，两个月过去了，进展如何？

一个有关数学形式化的有趣故事。

原标题：让AI理解费马大定理的证明，两个月过去了，进展如何？
文章来源：机器之心
内容字数：7468字

费马大定理证明的计算机形式化验证：一个充满挑战与惊喜的故事

本文总结了伦敦帝国学院Kevin Buzzard教授及其团队尝试用计算机验证费马大定理证明的进展，以及过程中遇到的挑战和意外收获。

1. 项目目标与现状

   Buzzard教授团队的目标是教计算机理解费马大定理（FLT）的现代证明，而非怀尔斯最初的证明。他们使用Lean证明器及其数学软件库mathlib进行形式化验证。目前，团队已完成部分抽象代数结果的证明，但仍未完成对关键概念“R”和“T”的完整定义。

2. 形式化验证的意义

   该项目旨在探索AI是否能革新数学研究，并检验Lean证明器在现代数论研究中的作用。通过形式化验证，计算机可以更好地理解现代数学定义，从而辅助人类突破数论难题。

3. 晶体上同调与除幂理论

   团队在形式化过程中遇到了一个意想不到的挑战：现代FLT证明中使用的晶体上同调理论，其基础——除幂理论，在标准文献中存在一个关键引理的错误。这个错误并非证明主要结论错误，但阻碍了形式化过程。

4. 发现错误与修正

   团队成员Antoine Chambert-Loir发现了文献中除幂理论的错误。这个错误并非微不足道，它影响了整个晶体上同调理论，甚至波及到Scholze等数学家的相关工作。然而，经过进一步研究，他们找到了Berthelot-Ogus著作附录中另一个正确的证明，解决了这个问题。

5. 挑战与反思

   这个故事揭示了现代数学文献中存在的文档化问题，许多被认为是“专家已知”的内容并未得到充分记录。该项目强调了形式化数学的重要性，它能显著降低错误的可能性。同时，它也说明了即使是重要的数学结论，其证明细节也可能存在疏漏，需要不断完善。

6. 圆满结局与未来展望

   最终，团队成员Maria Ines解决了除幂理论的形式化问题，项目得以继续推进。这个故事提醒人们重视数学的精确记录，并为未来计算机辅助数学研究提供了宝贵经验。

总而言之，Buzzard教授团队的尝试不仅在费马大定理证明的形式化验证方面取得了进展，更重要的是，它凸显了形式化数学在提高数学精确性和推动数学发展中的重要作用，以及现代数学文献中需要进一步改进的地方。

联系作者

文章来源：机器之心
作者微信：
作者简介：专业的人工智能媒体和产业服务平台