在陶哲轩的启发下，一批数学家决定以人工智能的方式来形式化费马大定理的证明

luyuanhong

在陶哲轩的启发下，一批数学家决定以人工智能的方式来形式化费马大定理的证明，将这个古老的问题带入数字时代

原创 mydear 麦田 人工智能中文站 2024-05-02 22:46 浙江

在陶哲轩的启发下，越来越多的数学家开始勇敢地踏入人工智能的领域，以此来开拓数学的新境界。他们的目光此刻聚焦在世界数学史上最具挑战性的难题之一：费马大定理。

如今，借助人工智能的力量，数学家们希望能够为费马的猜想画上圆满的句号。他们相信，AI 能够提供一种全新的方法来审视这个问题，可能会揭示出之前被忽略或难以察觉的数学规律和关联。

这场探索的道路充满了挑战和未知，但数学家们信心满满，他们相信，通过人工智能的帮助，费马大定理的谜团终将被揭开，为数学史上留下又一个辉煌的篇章。



费马大定理，又称「费马最后的定理（Fermat's Last Theorem，FLT）」，由 17 世纪法国数学家皮耶·德·费马提出。它的背后是一段传奇的故事。据说，大约在 1637 年左右，费马在阅读丢番图《算术》的拉丁文译本时，在第 11 卷第 8 命题的旁边写下了这样一段话：“将一个立方数分成两个立方数之和，或一个四次幂分成两个四次幂之和，或者一般地将一个高于二次的幂分成两个同次幂之和，这是不可能的。关于此，我确信已发现了一种美妙的证法，可惜这里空白的地方太小，写不下。”

这句话激发了无数数学家和研究者的好奇心和热情，然而，这个看似简单的陈述却隐藏着巨大的数学挑战。几个世纪以来，无数数学家们竭尽全力试图解决这个问题，但一直以来都未能找到令人满意的证明。



直到 1995 年，美国普林斯顿大学的 Andrew Wiles 教授经过 8 年的孤军奋战，终于用 130 页长的篇幅完成了证明。Wiles 也因此成为整个数学界的英雄。

费马大定理的证明是数学史上的一大里程碑，但这并不意味着数学家们的任务就此结束。相反，他们将目光转向了一个新的挑战：形式化费马大定理的证明。

数学的形式化是一项复杂而重要的工作，它通过使用严格的形式语言（如逻辑和集合论）来表述数学对象、结构、定理和证明，使其能够在计算机上进行表示、验证和操作，从而保证数学内容的准确性和一致性。

在去年年底，陶哲轩等人利用 Lean（一款交互式定理证明器，也是一门编程语言）形式化了他们的一篇论文，这篇论文是对多项式 Freiman-Ruzsa 猜想的一个版本的证明，于去年 11 月发布在 arXiv 上。在编写 Lean 语言代码的时候，陶哲轩还借助了 AI 编程助手 Copilot 。这一事件引起了数学界和人工智能界的广泛关注。



Kevin Buzzard 是 Lean 技术开源社区最重要的推广者之一，他也是伦敦帝国理工学院的教授。最近，他宣称要形式化费马大定理的证明，所用的工具也是 Lean 。

为什么要形式化费马大定理的证明？费马大定理的形式非常简洁、直观，然而证明它却异常艰难。这无疑是对数学深邃之美的一次绝佳展示。在过去的几个世纪中，为了解决这个问题，数学家们发展和创新了大量数学理论，这些理论在密码学到物理学等多个领域都有所应用。

Andrew Wiles 可能因 FLT 而受到启发，但他的工作实际上为朗兰兹计划带来了突破，该计划是数学中一系列影响深远的构想，联系数论、代数几何与约化群表示理论，且在 2024 年依然备受关注。

历史上，代数数论的其他几个重大突破（例如数域中的因式分解理论和循环域的算术）至少部分是出于对 FLT 更深层次理解的渴望。

Wiles 的工作，由他的学生 Richard Taylor 一起补充完整，建立在 20 世纪数学的庞大基础之上。Wiles 引入的基本技术——「模性提升定理（modularity lifting theorem）」——在原始论文发表后的 30 年间，在概念上被极大简化和广泛推广。这一领域至今仍然非常活跃。Frank Calegari 在 2022 年国际数学家大会上的论文，概述了自 Wiles 突破以来的进展。Kevin Buzzard 表示，这一领域的持续活跃，是他将 FLT 证明形式化的动机之一。

数学的形式化，即将纸上的数学转换为能够理解定理和证明概念的计算机编程语言的艺术。这些编程语言，也称为交互式定理证明器（ITP），已经存在了数十年。然而，近年来，这一领域似乎吸引了数学界的一部分关注。我们已经见证了多个研究数学形式。

你如果不方便使用魔法上网，可以使用我们站 AI ，国内直联，GPT4 最新 0125 版！

登录网址：

https://ai.weoknow.com

点击“阅读原文”，国内直达 GPT ，已经升级到 1 月 25 日的最新模型