数学历来是一门孤独的科学。
1986 年，安德鲁·怀尔斯（Andrew Wiles）为了证明费马大定理，遁入书斋长达七年之久。
数学家苦心孤诣得到的证明往往让同行难以理解，有些证明至今仍有争议。
但近年来，越来越多的数学领域被严格分解成各个组成部分，我们称之为「形式化」（formalized），这就可以让计算机来检查和验证数学证明。
菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩坚信，这些方法为数学领域的合作开辟了全新的可能性。
如果再加上人工智能的最新进展，在未来几年里，数学领域可能会出现全新的工作方式。
在计算机的帮助下，一些重大问题可能会被更快解决。
陶哲轩在接受《科学美国人》的德语姊妹刊物Spektrum der Wissenschaft的采访时阐述了他对未来的看法。
以下是采访实录——
「互不信任」的数学家通过AI建立合作
您在旧金山举行的联合数学会议上的一次演讲中，似乎暗示数学家之间互不信任。您这么说是什么意思？
我的意思是，你很难与素未谋面的人合作，除非你能逐行检查他们的作品。通常情况下，五个人是最多的合作人数。
随着自动校验器的出现，这种情况会发生怎样的变化？
现在，你真的可以与数百名素不相识的人合作。你不需要信任他们，因为他们上传代码，Lean编译器就会验证。你可以做比我们通常做的更大规模的数学。
当我用所谓的多项式（PFR）猜想形式化我们最近的成果时，我与20 多人一起工作。我们把证明分成了很多小步骤，每个人都为其中的一个小步骤贡献了证明。
我不需要逐行检查这些贡献是否正确。我只需要对整件事进行管理，确保一切都朝着正确的方向发展。这是一种不同的数学方式，一种更现代的方式。
德国数学家、菲尔兹奖得主Peter Scholze参与了一个Lean项目，尽管他告诉我，他对计算机并不了解。
在这些形式化项目中，并非每个人都需要成为程序员。有些人可以只专注于数学方向，你只是把一个大的数学任务分割成许多小块；有些人则专门负责把这些小部分转化为形式化证明。
我们不需要每个人都成为程序员，我们只需要一些人成为程序员。这是一种分工。
Peter Scholze的液体张量实验采用Lean 3作为项目背后的引擎
Lean将数学「形式化」
20 年前，我听说过机器辅助证明，当时它还是一个非常理论化的领域。每个人都认为，你必须从头开始——将公理形式化，然后做基础几何或代数，而要想进入高等数学，这超出了人们的想象。是什么让形式数学变得实用？
变化之一是标准数学库的开发。尤其是Lean。
有一个名为mathlib的庞大项目，所有本科数学的基本定理，如微积分和拓扑学等，都被一一收录到这个库中。
人们已经投入了大量的工作，将公理提升到相当高的水平。我们的梦想是把数学库真正提升到研究生教育的水平。这样，数学的形式化就会容易得多。
我们还期待有更好的搜索方法，因为如果你想证明某件事情，你必须能够找到有关的已经被证实为真的东西。因此，开发真正智能的搜索引擎也是一项重大的新进展。
所以这不是计算能力的问题？
不，一旦我们正式确定了整个PFR项目，编译验证只需要半个小时。这并不是瓶颈，瓶颈在于如何让人类使用它，如何提高可用性和用户友好度。
现在，我们已经有了一个由数千人组成的大型社区，而且还有一个非常活跃的在线论坛来讨论如何让这门语言变得更好。
