新智元报道
新智元报道
【新智元导读】自今年2月以来，AxiomProver已让8篇覆盖最硬核领域的AI论文现身arXiv，6篇正在筹备。上午出题下午交卷的节奏，让博士生秃头、教授评职称的日子一去不复返。接下来AI能做到什么？
数学家睡不着觉了！
想象你是一名审稿人。
有一天，一篇论文落到你手里。它声称证明了某个困扰同行几十年的难题。
你深吸一口气，泡上咖啡，开始逐行验算——可能要几个月，甚至好几年。
这并非夸张。
在数学界，硬核论文从投稿到见刊，等上两三年是家常便饭。
整个现代数学，建立在一套极其昂贵、极其缓慢、还偶尔出岔子的「人肉信用系统」上。
每一个「正确」背后，都是某个累得眼冒金星的人类专家在替它背书。
现在，数学家ken Ono说：这套系统，该升级了。
Ken Ono的这句话，含金量十足，他被美国数学学会前主席Ken Ribet称为「数学界的传奇人物」。
Ken Ono以对印度数学奇才拉马努金（Srinivasa Ramanujan）理论的深入研究而闻名，还带领了美国顶尖的本科研究项目，培养过10位Morgan Prize得主，Axiom创始人广州00后洪乐潼就是其中的一位。
这个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能做到什么？
参考资料：
编辑：大卫
