陶哲轩最新采访：AI将颠覆数学界！用Lean规模化，成百上千条定理一次秒杀

1,008 0 0

文章摘要

陶哲轩，一位菲尔兹奖得主及加州大学洛杉矶分校教授，在最近的采访中详细讨论了人工智能（AI）对数学领域的潜在影响。他对于使用如Lean这样的工具来“形式化”数学持乐观态度，并认为AI的辅助有潜力实现规模化生产，一次证明数百甚至数千条定理。尽管他预测数学问题在短期内不会被像国际象棋那样“解决”，但AI的发展有可能会提升人类科学家的洞察力。

数学一直被视为一种孤独的科学，历史上数学家们往往独自进行研究并得出让同行难以理解的证明。然而，近年来数学领域逐渐被分解并形式化，使得计算机能够检查和验证数学证明。陶哲轩认为，这为数学合作开辟了新的可能性，预示着未来数学工作方式的变革。

在采访中，陶哲轩提到了数学家之间合作的困难，通常因为难以信任未曾谋面的人。但随着自动校验器的出现，现在可以与数百名素不相识的人合作，因为他们上传的代码可以由Lean编译器验证。他通过形式化多项式（PFR）猜想，与20多人合作，将证明分成许多小步骤，每个人负责证明中的一小部分，而他则负责整体管理。

陶哲轩还提到了标准数学库的开发，尤其是Lean，它包含了所有本科数学的基本定理。他期望将数学库提升到研究生教育水平，使形式化数学变得更容易。此外，他也强调了开发智能搜索引擎的重要性，以便在证明过程中找到已被证实为真的相关事项。

尽管计算能力不是形式化数学的主要瓶颈，但如何提高可用性和用户友好度才是关键。目前，Lean拥有一个活跃的社区和在线论坛，讨论如何改进这门语言。陶哲轩认为，尽管Lean可能不是最先进的系统，但它拥有易于上手的特性、丰富的库和良好的社区支持。

关于形式化数学的未来发展，陶哲轩认为技术将越来越好，使得形式化过程不再耗时。他预见未来可能不再需要将证明打印出来，而是直接与AI如GPT交互，由AI在过程中尝试将其形式化。他想象将来一个大定理可能由20个人和一群AI共同证明，随着时间推移建立联系，创造出奇妙的成果。

陶哲轩也指出，尽管AI可能在三年内成为数学家的有用工具，成为出色的辅助工具，但他不认为数学会被“解决”。他认为，AI将帮助数学家更有效地探索问题空间，集中精力在真正关心的事情上。他还提到，尽管目前证明的想法必须来自人类数学家，但未来可能会有变化，可能存在一些合作项目，人们已经有了如何证明小部分内容的想法，他们会把这些想法形式化，并尝试组合在一起。

此外，陶哲轩认为，形式化数学可以使教科书更加交互，使一个领域的数学家更容易为另一个领域做出贡献。他还提到，数学家通常依赖别人已经证明的结果，他们知道为什么它是真的，但不必将其分解成公理。他认为，随着形式化的发展，人们将适应这种变化，不必检查所有事情，让电脑帮助核对。

最后，陶哲轩讨论了训练数学AI可能遇到的问题，包括缺乏足够的数据进行训练，因为很多灵感并非在期刊上的论文中捕捉到的。他提出，可能需要让AI接受标准的研究生教育，坐在课堂上学习，或者对证明的努力进行登记，以便训练未来的AI。他还指出，形式化将使隐性知识显性化，带来意想不到的好处。