RecodeX 重构消息，纽约大学阿布扎比分校博士后Rishikesh Gajjala宣布退出数学学术界。过去几个月，AI帮助他在读博期间钻研多年的难题上接连取得突破，但他认为数学的意义在于探索过程而非答案本身，AI正使答案变得廉价，因此决定转向形式化验证领域，加入获Khosla Ventures领投2700万美元种子轮的PramaanaLabs，用Lean定理证明助手语言形式化验证AI发现的猜想。

与此同时，Axiom Math的多智能体系统AxiomProver首次自动完成“246定理”证明的形式化验证，该定理代表人类关于素数知识的边界。团队还将素数间隙结果打包成开源库，供其他AI系统调用。陶哲轩在2026年国际数学家大会演讲中提出“证明的消化不良”概念，指AI生成证明速度远超人类审核速度。