16亿美元公司用AI智能体验证数学基石，过滤AI”垃圾”污染
AI突破数学难题背后的隐患
近期人工智能在数学领域展现出令人瞩目的进展，几乎每周都能见证新的突破。上个月，OpenAI一口气发布了719篇学术论文，声称攻克了数学界最为棘手的若干难题。然而，即便是用于确认这些成果的计算机验证程序也存在漏洞。经历了数年”AI生成垃圾”的洗礼，人们不禁要问：数学领域是否也难逃此劫？
在这一背景下，Axiom Math押注数学能够规避这一命运。他们并非通过减缓发展速度来应对，而是选择站在更坚实的基础之上。这家估值高达16亿美元的初创企业，致力于构建一个经过形式化验证的数学基石，让AI智能体能够依赖它来编写软件，并最终推动科学研究。
验证数学史上的里程碑之作
周三，该公司宣布已完成对”Stacks项目”的形式化验证。这是人类历史上体量最为庞大的数学著作之一，在数学家群体中享有极高声誉。
哥伦比亚大学数学家Peter Woit曾评价称，该项目”几乎无可替代”，并将其与著名的”布尔巴基丛书”相提并论——这套丛书在20世纪重建了整个数学的基础体系。
该项目的发起人Johan de Jong同样是哥伦比亚大学的数学家，于2005年发起这项开源计划。多年来，全球数学家持续贡献自己的力量，从大学水平的代数出发，逐步拓展至代数、几何和数论等领域的最前沿思想。
智能体构建千万行验证代码
该公司部署的智能体集群，将这个约7654页的知识库转化为约1600万行可被计算机验证的代码。
形式化验证的核心逻辑在于：数学家将证明过程改写为Lean编程语言，再由称为”证明助手”的程序逐行检查代码逻辑。若顺利通过，便可确信其逻辑严密无误。
这种思路同样广泛应用于工程领域。工程师利用形式化验证确保芯片设计万无一失，法国研究人员也曾用它发现计算家庭福利的软件中存在bug。
从粗放到精细：智能体的进化之路
对于Stacks项目这样的庞大知识库而言，逐一定理验证只是基础工作。项目中的定理与定义之间相互关联、层层递进，如同一棵家族树，多数成果都可追溯至早期基础定理。
正是这种高度互联性，最初让Axiom团队对项目的可行性存疑。他们需要确保约1600万行Lean代码中每一条关联链路都完好无损。
Axiom CEO Carina Hong向媒体坦言：”体量庞大与结构精密的事物往往难以兼得。而Stacks正是数学的根基，你必须确保其中的定理保持一致、不存在悖论，定义之间也不能相互冲突。”
这位年仅25岁的CEO曾是斯坦福大学数学博士项目的学生，于2025年3月辍学创业。同年3月，Axiom成功募集2亿美元A轮融资，由Menlo Ventures领投。
“我们最初并不确信’氛围编程’能否完整保留Stacks的美学价值，”Hong表示。
并行协作释放智能体潜力
为完成这一宏大工程，团队为智能体设定了大致框架后便让它们并行运行。
Axiom技术团队成员Ashvin Swaminathan解释道：”我们在Stacks项目中设置了层级结构，但这并非事无巨细地指挥每个智能体的操作方式。智能体自主寻找任务，识别可以并行处理的工作内容。”
值得一提的是，Axiom还专门训练了自身擅长的数学模型——这一路径是大多数同类验证初创公司未曾涉足的。起初，团队依靠内部Lean专家向智能体传授”人类品味”，但随着时间推移，智能体逐渐形成了自己的判断力。
填补代数几何形式化空白
这项成果填补了形式化数学领域最大的空白之一。
Swaminathan指出：”审视当前已形式化的数学成果，存在一个巨大的黑洞，而这个黑洞恰好覆盖了代数几何领域。”他补充道，在此之前，希望用Lean验证代数几何新成果的研究者几乎无从下手，”但现在，他们有了基础。”
Axiom坚信，每个经过验证的定理都将成为一块基石，未来的证明工作可以依托这些经过检验的数学成果，而非每次都从零开始。 UCLA数学家、菲尔兹奖得主Terence Tao也对这一方向给予了关注。
关注微信号：智享开源 ，及时了解更新信息。
公众号：智享开源
还没有任何评论，你来说两句吧！