公司概况与融资 - 初创公司Axiom Math由24岁的Carina Hong创立，致力于开发能够自主验证逻辑正确性的“AI数学家” [1] - 公司在2025年10月完成6400万美元种子轮融资，由B Capital领投，估值达3亿美元 [4][7] 核心技术与方法 - 与主流大模型不同，其系统通过Lean编程语言确保推理过程的每一步都可追溯、可检查，解决了AI产出结果难以验收的信任难题 [1][21] - 公司方法的核心是让AI不仅能生成答案，还能自己验证对错，追求结果的可信度而非仅仅是能力 [4][18][24] - 2025年12月，其系统AxiomProver在美国Putnam数学竞赛中自主解决了9道题（共12道），并在Lean语言中给出了全部通过验证的形式化证明 [23] 团队构成与人才吸引力 - 核心团队汇聚了来自Meta FAIR和Google Brain的前核心研究员等顶尖技术人才 [1][4] - 创始人Carina Hong在MIT的导师、57岁的知名数学家Ken Ono辞去弗吉尼亚大学终身教职，全职加入公司担任创始数学家 [4][29] - 团队规模目前为17人，成员被“用AI做出可验证的数学成果”的愿景所吸引，而非追求产品热潮 [27][30][31] 产品愿景与行业意义 - 公司目标不是制造聊天机器人或代码助手，而是打造一个能验证定理、提出新猜想的AI系统 [14] - 旨在将AI从不稳定的辅助工具提升为能在科研与工业领域真正落地、可被验收的可靠合作者 [1] - 公司押注于AI的“下一个及格线”，即从追求能力转向建立可信度 [8][41] - 其标准一旦成立，将推动AI在容错率低的场景（如芯片设计、科学研究、金融系统）中成为可信任的合作者 [24][40][42] 研发进展与能力展示 - 在研究Collatz猜想时，其Transformer模型对万亿级数字序列的预测准确率达到99.8%，且错误能被清楚解释 [33] - 公司规划AI探索数学的三个阶段：用形式语言表达定理、验证旧问题的新解法、提出新猜想并给出数学依据 [35][36][37] - 相信AI可以将数学研究的进展周期从十年缩短到几个月 [39]