自今年2月以来，AxiomProver已让8篇覆盖最硬核领域的AI论文现身arXiv，6篇正在筹备。上午出题下午交卷的节奏，让博士生秃头、教授评职称的日子一去不复返。接下来AI能做到什么？

数学家睡不着觉了！

想象你是一名审稿人。

有一天，一篇论文落到你手里。它声称证明了某个困扰同行几十年的难题。

你深吸一口气，泡上咖啡，开始逐行验算——可能要几个月，甚至好几年。

这并非夸张。

在数学界，硬核论文从投稿到见刊，等上两三年是家常便饭。

整个现代数学，建立在一套极其昂贵、极其缓慢、还偶尔出岔子的「人肉信用系统」上。

每一个「正确」背后，都是某个累得眼冒金星的人类专家在替它背书。

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

Ken Ono的这句话，含金量十足，他被美国数学学会前主席Ken Ribet称为「数学界的传奇人物」。

Ken Ono以对印度数学奇才拉马努金（Srinivasa Ramanujan）理论的深入研究而闻名，还带领了美国顶尖的本科研究项目，培养过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能做到什么？

参考资料：

https://x.com/axiommathai/status/2059640252546126087?s=20https://www.axios.com/2026/05/26/axiom-ai-math-journalhttps://axiommath.ai/papers