降维打击，数学博士熬秃头，AI数学家：上午出题，下午4点交证明

数学家睡不着觉了！

想象你是一名审稿人。有一天，一篇论文落到你手里，声称证明了某个困扰同行几十年的难题。你深吸一口气，泡上咖啡，开始逐行验算——接下来可能要搭进去几个月，甚至好几年。

这并非夸张。在数学界，硬核论文从投稿到见刊，等上两三年是家常便饭。整个现代数学，建立在一套极其昂贵、极其缓慢、还偶尔出岔子的「人肉信用系统」上。每一个「正确」背后，都是某个累得眼冒金星的人类专家在替它背书。

现在，数学家Ken Ono说：这套系统，该升级了。

Ken Ono这句话的含金量，从圈子里的反应就能看出来——他被美国数学学会前主席Ken Ribet称为「数学界的传奇人物」。这位以深入研究印度数学奇才拉马努金理论而闻名的学者，还带领过美国顶尖的本科研究项目，培养出10位Morgan Prize得主。值得一提的是，Axiom创始人、广州00后洪乐潼，就是其中的一位。

一个上午就能解开难题的AI

这个AI工具叫AxiomProver。它有多猛？

自今年2月以来，已有8篇论文悄悄出现在arXiv（全球数学家扔预印本的地方）上，覆盖代数几何、表示论、数论、组合数学这几个最硬的领域。其中5篇已被权威数学期刊接收，另有多篇正在期刊审查中，还有6篇在筹备。

据他们团队所知，以这种方式把「论文+形式化证明证书」引入期刊文献，在历史上还是头一回。

但真正让人头皮发麻的，是速度。有时候，数学家上午10点丢给系统一个尚未解决的开放研究问题，当天下午4点，AI就能给出一份完整的、经过机器验证的证明。上午出题，下午交卷，中间隔着一顿午饭的工夫。这要搁过去，是一篇能让博士生熬秃头、让教授评上职称的成果。

它凭什么「不会算错」？

聊到这你可能会皱眉：AI不是经常一本正经地胡说八道吗？这玩意儿，凭什么信它？

问得好。这恰恰是整件事最关键的地方。普通的大语言模型（就是你天天用的那种聊天AI），本质上是在「猜」下一个最可能的词。猜得多了自然会出错——它们刚出道那会儿，连小学算术都能算砸，被人嘲笑了好一阵。

但AxiomProver走的是另一条路。它生成的证明，全部用一种叫Lean的形式化语言写成。

Lean是什么？你可以把它理解成一个铁面无私、毫无情商的机器裁判。它不在乎你的证明读起来多优雅、思路多巧妙，只认一件事：每一步推理在逻辑上是不是严丝合缝。差一个符号，对不起，不通过。

所以，AxiomProver证明的「正确性」，不再依赖某个人类专家熬夜帮你检查，而是由机器当场盖章背书。它没法蒙混过关，因为一旦写错，机器自己当场就知道。人类审稿人会累、会困、会看走眼，机器裁判不会。

数学的「信用危机」和「速度瓶颈」在崩塌

讲到这，我们可以把这事的真正分量摊开说了。科学发现长期卡在两个老大难问题上。

第一个是信用危机。数学证明到底对不对，最终要靠人来拍板。但人会犯错、有立场、精力有限，这套「靠人背书」的系统本质上是脆弱的。

第二个是速度瓶颈。审稿动辄数年，不是因为审稿人懒，而是人脑验算的速度就是这么慢。再聪明的脑子，一天也只有24小时。

AxiomProver这套打法，等于同时朝这两个痛点开了一枪。信用问题交给机器：Lean检查器盖的章比任何人类专家都可靠。这就是期刊审稿能快得吓人的原因——审稿人不必再从零验算，只需判断这成果重不重要、写得好不好。速度问题交给算力：上午出题下午交卷，这种节奏在人类时代是天方夜谭。

AI这次引起的震动，数学界感知最深。去年10月，OpenAI宣称GPT-5「解决」了10个埃尔德什难题，数学界直呼造假，Demis Hassabis称其「令人尴尬」。7个月后，OpenAI和DeepMind竟在同一周内，双双发布了经过验证的数学突破。而Axiom想做的，是把数学从「手工作坊」的农业时代，推进到「即时验证、机器背书」的工业化时代。

那么，接下来AI能做到什么？这才是真正值得期待的问题。