数学家Ken Ono最近抛出一个让同行失眠的问题：如果AI能在一顿饭的工夫解决困扰人类几十年的难题，数学界引以为傲的审稿系统还撑得住吗？这位被美国数学学会前主席称为传奇人物的数学家，正见证着自己培养的学生洪乐潼创办的Axiom公司，用一款名为AxiomProver的AI工具，对传统数学研究模式发起降维打击。自今年2月以来，已有8篇覆盖代数几何、表示论、数论和组合数学的AI论文悄然出现在arXiv上，其中5篇被权威期刊接收，另有6篇正在筹备。这不是科幻小说，而是正在发生的现实。

AxiomProver最令人震撼的是其恐怖的速度。据报道，数学家上午10点丢给系统一个尚未解决的开放问题，当天下午4点就能收到一份完整的、经过机器验证的证明。中间只隔着一顿午饭的时间。而这样的成果，在过去足以让一名博士生熬秃头、让教授评上职称。传统数学论文从投稿到见刊，等上两三年是家常便饭，整个现代数学建立在一套极其昂贵、极其缓慢、还偶尔出岔子的人肉信用系统上。每一个正确背后，都是某个累得眼冒金星的人类专家在替它背书。

你可能会问：AI不是经常一本正经地胡说八道吗？凭什么相信它？这正是整件事最巧妙之处。普通大语言模型本质上是在猜下一个最可能的词，猜多了自然会出错。但AxiomProver走的是另一条路——它生成的证明全部用Lean形式化语言写成。Lean就像一个铁面无私的机器裁判，不在乎证明读起来多优雅，只认一件事：每一步推理在逻辑上是否严丝合缝。差一个符号，对不起，不通过。这意味着AxiomProver无法蒙混过关，一旦写错，机器自己当场就知道。人类审稿人会累、会困、会看走眼，机器裁判不会。

这场变革直击科学发现的两大痛点：信用危机和速度瓶颈。传统数学审稿依赖人类专家逐行验算，但人会犯错、有立场、精力有限。AxiomProver将信用问题交给机器，Lean检查器盖的章比任何人类专家都可靠；将速度问题交给算力，上午出题下午交卷的节奏在人类时代是天方夜谭。去年10月，OpenAI宣称GPT-5解决了10个埃尔德什难题，数学界直呼造假。7个月后，OpenAI和DeepMind竟在同一周内双双发布经过验证的数学突破。如今Axiom想做的，是把数学从手工作坊的农业时代，推进到即时验证、机器背书的工业化时代。接下来AI能做到什么？或许很快，数学家的工作将从证明难题，转变为提出好问题。