跨越300多年的接力：受陶哲轩启发，数学家决定用AI形式化费马大定理的证明

AIGC动态8个月前发布 almosthuman2014

1,042 0 0

文章摘要

【关键词】 费马大定理、AI数学探索、形式化证明、Lean定理证明器、数学研究

在数学界，人工智能的应用正在逐渐扩展，特别是在数学探索和证明方面。近年来，受到陶哲轩等人的启发，越来越多的数学家开始尝试利用人工智能，特别是定理证明器，来进行数学问题的研究。本文报道了数学家们尝试利用人工智能对费马大定理（Fermat’s Last Theorem，FLT）进行形式化证明的尝试。

费马大定理是17世纪由法国数学家皮耶・德・费马提出的，它指出当整数n>2时，方程x^n + y^n = z^n没有正整数解。费马声称自己找到了证明方法，但未曾公布。这个问题悬而未决长达300多年，直到1995年，美国数学家Andrew Wiles提出了一个长达130页的证明，解决了这一难题。

尽管费马大定理已经被证明，但数学家们现在希望利用人工智能进一步形式化这一证明。形式化证明是指使用计算机语言将数学内容表述得更加严格和精确，以便在计算机上进行验证和操作。去年，陶哲轩等人已经使用Lean定理证明器形式化了他们对多项式Freiman-Ruzsa猜想的证明，这一事件引起了数学界和人工智能界的广泛关注。

伦敦帝国理工学院的Kevin Buzzard教授是最近宣称要形式化费马大定理证明的数学家之一。他的动机是，费马大定理的证明不仅是数学之美的展示，而且在数学的发展中起到了推动作用，特别是在朗兰兹计划中。他认为，通过形式化这一证明，可以帮助计算机更好地理解现代数学研究中的概念。

Buzzard的项目已经启动，并得到了EPSRC的资助。他的目标是将费马大定理的证明简化为1980年代数学家已知的形式，并邀请其他数学家参与到这一项目中。他认为，通过形式化证明，可以将证明分解为许多小引理，从而便于众包和协作。

为了参与项目，数学家需要了解Lean定理证明器的知识。Buzzard推荐了在线教科书《Mathematics in Lean》作为学习资源。项目将在Lean Zulip chat的FLT stream上进行，这是一个数学家和计算机科学家可以实时协作的研究论坛。

此外，Lean定理证明器本身也在不断发展，最新的Lean 4版本进行了多项优化，提高了编译速度和错误处理能力。去年，LeanDojo团队和加州理工学院的研究者还推出了Lean Copilot，这是一款专为大型语言模型与人类交互而设计的协作工具，为数学研究注入了AI大模型的力量。

陶哲轩对人工智能在数学研究中的应用持乐观态度，并预言到2026年，AI将成为数学研究的值得信赖的合著者。随着人工智能技术的发展，数学家们对于AI在数学探索中的潜力抱有期待，希望能够实现更多的突破。