自今年2月起，AxiomProver已悄然在arXiv上线8篇横跨最艰深数学方向的AI驱动论文，另有6篇正处于紧锣密鼓的撰写阶段。上午抛出问题、下午交付完整证明——这种节奏，正让博士生告别通宵改稿，也让教授职称评审不再仰赖十年磨一剑。
数学家开始失眠了！
试想你是一位期刊审稿人。
某天，一封投稿邮件抵达邮箱。标题直指一个悬而未决数十年的核心难题。
你屏住呼吸，煮好浓咖啡，翻开第一页……然后可能耗尽数月甚至数年，逐行复核每一个引理、每一步推导。
这不是戏剧化渲染。
在当代数学出版体系中，一篇高难度论文从提交到正式见刊，等待两三年实属常态。
整座现代数学大厦，稳稳矗立于一套极其昂贵、极度低效、且偶有疏漏的「人工信用机制」之上。
每一个被标注为「已验证」的结论，背后都站着一位双眼布满血丝、反复校验至极限的人类权威。
如今，数学家Ken Ono断言：这套机制，是时候迭代升级了。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜
Ken Ono这句判断分量极重。他曾被美国数学学会前主席Ken Ribet誉为「数学界真正的传奇」。
他以深度挖掘印度天才拉马努金（Srinivasa Ramanujan）遗留理论而广受尊敬，同时执掌全美顶尖本科数学研究项目，已指导出10位Morgan Prize获奖者——Axiom创始人、广州出生的00后洪乐潼，正是其中一员。
一个上午就能攻克开放问题的AI
这款工具名为AxiomProver。
它究竟有多强？
公开信息显示，自今年2月以来，已有8篇覆盖代数几何、表示论、数论与组合数学等公认“硬核顶峰”领域的论文，悄然登上arXiv——全球数学家发布预印本的核心平台。
其中5篇已被国际权威数学期刊正式接收，其余多篇处于同行评议流程中，另有6篇正在加速筹备。
据团队确认，将「学术论文+机器可验证的形式化证明证书」同步提交至传统期刊并获采纳，这在全球数学出版史上尚属首次。
但真正令人震撼的，是它的响应速度。
有时，数学家上午10点向系统输入一个尚未解决的前沿开放问题；当天下午4点，AI便输出一份逻辑严密、全程由机器验证无误的完整证明。
上午出题，下午交卷，中间只隔一顿午饭的时间。
放在过去，这足以撑起一位博士生的整个毕业答辩，或成为教授晋升的关键成果。
它为何能“零容错”？
看到这里你或许会质疑：当前大模型不是常犯低级错误吗？这样的AI，凭什么让人信服？
这个问题切中要害——也恰恰是本次突破的核心所在。
常规大语言模型（即日常使用的对话式AI），本质是在概率层面预测下一个最可能出现的词。
预测多了，自然难免失准——早期版本甚至会在基础算术上翻车，一度引发学界广泛调侃。
而AxiomProver走的是截然不同的技术路径：它生成的所有证明，均以Lean这一形式化语言严格书写。
Lean是什么？
你可以把它看作一位冷面无情、毫无妥协余地的逻辑仲裁员。
它不关心你的证明是否文采斐然、思路是否惊艳绝伦，唯一关注的只有一件事：每一步推理是否在公理系统内绝对自洽。哪怕符号错一位、括号少一对，立刻驳回，绝不通融。
因此，AxiomProver所产出的「正确性」，不再依赖某位人类专家挑灯夜战式的审查，而是由机器在毫秒级完成即时认证与盖章。
它无法蒙混过关——因为任何偏差，都会被Lean当场识别并拦截。
人类审稿人会疲惫、会分神、会遗漏细节；机器裁判不会。
数学的「信任赤字」与「效率天花板」正在瓦解
讲到这里，这项进展的真实意义已然清晰。
科学进步长期受制于两大结构性瓶颈：
其一是信任赤字。
数学证明的终极真理性，最终仍需人类专家签字背书。但人非圣贤，存在认知局限、主观倾向与精力边界，这套“以人为锚”的验证体系，本质上并不牢靠。
其二是效率天花板。
动辄以年计的审稿周期，并非源于审稿人懈怠，而是人脑推演与核查的速度天然受限。再卓越的大脑，一天也只有24小时。
AxiomProver的实践，正同步击穿这两大桎梏。
信任交给机器：Lean验证器出具的认证，比任何个体专家更具公信力与可复现性。
这也是期刊审稿得以大幅提速的根本原因——编辑与审稿人无需重走全部推导链，只需聚焦于成果的原创性、重要性与表述质量。
效率交给算力：上午提问、下午得证，这种节奏在纯人力时代近乎神话。
AI正在撼动数学界的根基。
去年10月，OpenAI曾宣称GPT-5“攻克”10个埃尔德什难题，结果遭数学界集体质疑为虚假宣传，Demis Hassabis亦称其“相当尴尬”。
仅7个月后，OpenAI与DeepMind竟在同一周内，各自发布了经形式化验证的实质性数学突破。
而Axiom的目标更为深远：推动数学从依赖个体直觉与手工验证的“手工作坊”时代，迈入支持实时验证、机器确权的“工业化”新纪元。
接下来AI还能做到什么？
参考资料：
https://www.php.cn/link/0532f44875bec555073a20e30b3c50f4
https://www.php.cn/link/269dce383b169909785f4fda1ed47913
https://www.php.cn/link/597949a90178337ebb9bc18d3dae6a59
本文来自微信公众号“新智元”，作者：ASI启示录，编辑：大卫，36氪经授权发布。
