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

AIGC动态欢迎阅读

原标题：陶哲轩最新采访：AI将颠覆数学界！用Lean规模化，成百上千条定理一次秒杀
关键字：数学,人工智能,数学家,人类,领域
文章来源：新智元
内容字数：0字

内容摘要：

新智元报道编辑：庸庸乔杨
【新智元导读】陶哲轩在最新的采访中，系统地谈到了AI可能会对数学领域产生的影响。他乐观地认为，使用Lean等工具「形式化」数学，在AI的辅助下实现规模化生产——一次证明数百或数千条定理。但他也审慎地预测，数学问题在短期内不会像国际象棋一样被「解决」，但有可能会提高人类科学家的洞察力。数学历来是一门孤独的科学。
1986 年，安德鲁·怀尔斯（Andrew Wiles）为了证明费马大定理，遁入书斋长达七年之久。
数学家苦心孤诣得到的证明往往让同行难以理解，有些证明至今仍有争议。
但近年来，越来越多的数学领域被严格分解成各个组成部分，我们称之为「形式化」（formalized），这就可以让计算机来检查和验证数学证明。
菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩坚信，这些方法为数学领域的合作开辟了全新的可能性。
如果再加上人工智能的最新进展，在未来几年里，数学领域可能会出现全新的工作方式。
在计算机的帮助下，一些重大问题可能会被更快解决。
陶哲轩在接受《科学美国人》的德语姊妹刊物Spektrum der Wissenschaft的采访时阐述了他对未来的看法。
以下