【导语顶尖数学学者Rishikesh Gajjala靠AI攻破博士课题后却宣布退出学术圈转身投入形式化验证领域。与此同时Axiom Math用多智能体系统完成“246定理”证明的形式化验证数学界正经历着AI带来的巨大变革。】AI突破难题学者却选择退场刚从纽约大学阿布扎比分校做完博士后的Rishikesh Gajjala在过去几个月里借助AI在博士期间钻研多年的难题上接连取得突破。然而他却在X上宣布离开数学学术界。对他来说数学的意义在于探索答案的过程而如今AI让答案变得唾手可得他觉得自己在其中越来越像个多余的人。证明过剩信任成难题随着AI智能的不断增强和成本降低数学论文如洪水般涌现但缺乏验证。当世最伟大的数学家之一陶哲轩提出“证明的消化不良”指出AI生成证明的速度远超人类审核速度数学正从证明稀缺时代进入证明过剩时代。Gajjala也认为在通过验证之前一份漂亮的证明和垃圾没有区别。转身验证领域成果初现想透这一切后Gajjala决定投身形式化验证领域用Lean语言把借助LLM发现的长期猜想和Erdős问题形式化。他加入了PramaanaLabs研究重心从“发现数学真理”换成“构建能证明AI答案正确的认证系统”。同一时间Axiom Math用自家多智能体系统AxiomProver首次自动完成了“246定理”证明的形式化验证。246定理人类素数知识的边界“246定理”代表着人类目前关于素数知识的绝对边界。孪生素数猜想提出不管沿着数轴走多远总会有相差为2的素数对出现但至今无人能证明。2013年张益唐证明存在无穷多对相差不超过7000万的素数之后James Maynard和陶哲轩等人不断缩小差距最终将间隙压到了246。AxiomProver验证了这条定理并将素数间隙的一批结果打包成可复用的开源库。AI时代验证角色成刚需一位数学学者退出学术圈看似只是个人选择但背后反映出这个世界即将运行在没人读过的代码之上。陶哲轩也表示对未来趋势的预测变得不确定。Gajjala从找真理的人变成给真理盖章的人在AI加速重写一切的时代这样的验证角色可能才是最紧缺的。编辑观点AI在数学领域的应用带来了突破但也引发了信任危机。Gajjala的选择和Axiom Math的成果都凸显了验证环节的重要性未来数学界或许将更加依赖可靠的验证系统。