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

文章预览

单击上方“ 图灵人工智能 ”，选择“星标”公众号 您想知道的人工智能干货，第一时间送达   转自 新智元   编辑：庸庸 乔杨 【导读】 陶哲轩在最新的采访中，系统地谈到了AI可能会对数学领域产生的影响。 他乐观地认为， 使用 Lean 等工具「形式化」数学，在AI的辅助下实现规模化生产——一次证明数百或数千条定理。 但他也审慎地预测，数学问题在短期内不会像国际象棋一样被「解决」，但有可能会提高人类科学家的洞察力。 数学历来是一门孤独的科学。 1986 年，安德鲁·怀尔斯（Andrew Wiles）为了证明 费马大定理 ，遁入书斋长达七年之久。 数学家苦心孤诣得到的证明往往让同行难以理解，有些证明至今仍有争议。 但近年来，越来越多的数学领域被严格分解成各个组成部分，我们称之为「形式化」（formalized），这就可以让计算机来检查和 ………………………………