新智元曾有报道
一位顶尖数学家利用AI，在短短几个月内接连攻克了困扰自己多年的博士课题。
这样的成就本应被视为好事。
但令人意外的是，他竟然宣布退出学术圈。
这位学者名为 Rishikesh Gajjala，刚刚完成在纽约大学阿布扎比分校的博士后工作。
就在昨日，他在X平台上发布了一张引发整个数学界震动的帖子：我决定离开数学学术界。
过去数月间，AI帮助他在读博期间反复思索、最为看重的那些问题上不断获得突破性进展。
如果按照常规进度，这些难题需要他耗费数年时间才能有所进展。换作常人，这应该会更加坚定他对数学的信念。
但结果却完全不同。每周过去，他都会感觉自己在数学领域越来越显得无所事事。
Gajjala表示，数学对他而言，意义从来不在最终答案上。而在答案揭晓之前那般漫长甚至数年的探索过程，那些被一一排除的蹊径，持续的苦苦钻研，直至隐藏的结构终于显露。正是那段奋斗经历让成果真正属于他自己。
如今他认定，我们正迅速步入一个时代：上帝之书的诸多答案，或许只需一个指令 prompt 即可获取。
想通这一层之后，将大半生时间都用来比别人早一点找到那些答案上，他突然觉得失去了价值。
尽管有一个问题始终萦绕在他心头。
如何确认这个由AI给出的神圣判断是正确的？
智能系统正变得一日强于一日，价格也日渐亲民，数学论文则铺天盖地而来。但没有经过验证。
这些AI系统生成的证明可能极为精巧。同样，错误也可能隐藏得极为隐蔽。
评估一个看似完美的突破是否成立，有时需要耗费他数日时间。
Gajjala放了一句"狂言"：未经验证的漂亮证明和毫无价值的证明一样。
这番话虽显刺耳，却并非只有他一人这么想。
数学界最伟大的学者之一陶哲轩，在即将举行的2026年国际数学家大会（ICM）上特别做了题为《AI时代的数学》的演讲，内容几乎与上述观点一致。
他创造了一个新词叫做"证明的消化不良"（proof indigestion）——AI生成证明的速度已经远远超过人类审核的速度，数学正从一个证明稀缺的时代迈入一个证明泛滥的时代。
他特别指出，一个专门收集数学难题的网站上，已经充斥着大量AI生成的证明提交。许多可能正确，却无暇被人类数学家逐一核实。
说白了，AI撰写论文的速度快如闪电，而人类阅读论文的速度还是那般缓慢。当论文如潮水般涌来，那些无人翻阅的"正确答案"，与不存在并无区别。
智能正在成为最廉价的产物，而能够被信任的智能，依然是极其珍贵的。
从寻找答案到创造验证体系
经过深思熟虑，Gajjala作出了一个决定：不再寻找答案，而是去构建能够为答案提供认证的体系。
他随即转入形式化验证领域，使用Lean（一种定理证明助手语言）将那些借助LLM发现的长期猜想和Erdős问题一一形式化。
接着他加入了刚刚获得Khosla Ventures领投2700万美元种子轮的PramaanaLabs，研究重心从"发现数学真理"转变为"构建能够证明AI答案正确的认证系统"。
有读者在评论区询问Gajjala：AI很快也能以超乎常人的速度制造出验证系统本身吧？
他回复道：我对此还抱有怀疑。如果哪天我真的这么认为，我就再找一份新工作。
形式化验证就是将证明改写成机器可以理解的语言，让计算机逐行进行核查。
人类会看漏细节，会感到疲倦，甚至可能被作者的优美文辞所迷惑。但机器在逐行校验时不受情绪影响，不会被作者的写作技巧所左右。
就在此时，这条道路上取得了迄今为止最丰硕的成果。
246定理
人类距离孪生素数最近的理论边界
Axiom Math公司运用其多智能体系统AxiomProver，首次完成了"246定理"证明的形式化验证。
创始数学家Ken Ono表示，这个定理代表着人类目前关于素数了解的绝对极限。
246意味着什么？
2、3、5、7、11、13……随着素数的增加其出现的频率逐渐降低，但总有些素数彼此相距极近，例如3与5、11与1
网友评论