陶哲轩最新访谈：人工智能将在几年内变革数学研究！

文章预览

数学研究，在许多时候都是一项孤独的工作。 张益唐 远离数学圈 20 年，独自一人潜心思考孪生素数猜想；佩雷尔曼“隐退”长达七年，全身心投入到庞加莱猜想的攻克中，除了偶尔在超市与店员的交集外，他几乎与世隔绝；；安德鲁·怀尔斯 (Andrew Wiles) 隐居在书房里用了七年时间证明费马大定理……   图丨张益唐（来源：University of New Hampshire） 这种孤独，在一定程度上源于解决问题所需的深度专注 与沉浸，也是因为，他们各自的思索，在很多时候难以向其他人言明与分享。 但近年来，这种状况正在发生改变。 随着交互式定理证明工具（interactive theorem prover，ITP）等计算机工具与  AI 技术的发展，数学领域中越来越多的部分被精细地拆解为各个组成部分，从而转换为能够让计算机理解定理和证明概念的编程语言，这一过程，即为“形式化”（fo ………………………………