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

AIGC动态6个月前发布 AIera
951 0 0
陶哲轩最新采访:AI将颠覆数学界!用Lean规模化,成百上千条定理一次秒杀

 

文章摘要


【关 键 词】 人工智能数学合作形式化数学数学教育技术发展

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

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

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

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

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

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

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

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

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

“极客训练营”

原文和模型


【原文链接】 阅读原文 [ 5007字 | 21分钟 ]
【原文作者】 新智元
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★★★

© 版权声明
“绘蛙”

相关文章

暂无评论

暂无评论...