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

文章预览

来源：FUTURE | 远见 选编：FUTURE | 远见 闵青云  陶哲轩在最新的采访中，系统地谈到了AI可能会对数学领域产生的影响。他乐观地认为，使用Lean等工具「形式化」数学，在AI的辅助下实现规模化生产——一次证明数百或数千条定理。但他也审慎地预测，数学问题在短期内不会像国际象棋一样被「解决」，但有可能会提高人类科学家的洞察力。 数学历来是一门孤独的科学。 1986 年，安德鲁·怀尔斯（Andrew Wiles）为了证明费马大定理，遁入书斋长达七年之久。 数学家苦心孤诣得到的证明往往让同行难以理解，有些证明至今仍有争议。 但近年来，越来越多的数学领域被严格分解成各个组成部分，我们称之为「形式化」（formalized），这就可以让计算机来检查和验证数学证明。 菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩坚信，这些方法为数学领域的 ………………………………