数学家因AI突破退圈，转向验证系统构建

新智元 · wechat · 2026-08-18

数学学者Rishikesh Gajjala因AI在数月内攻克其多年课题，认为探索过程价值被稀释，决定离开学术界投身形式化验证领域，加入Pramaana Labs。陶哲轩此前提出“证明消化不良”概念，指出AI生成证明速度远超人类审核能力，导致数学进入“证明过剩”时代。与此同时，Axiom Math利用多智能体系统完成了人类离孪生素数猜想最近的“246定理”形式化验证，并开源了相关素数研究库，为未来AI数学研究提供经过机器验证的基础设施。