1. AI 真的能搞数学了？
这消息出来，圈子里挺炸锅的。一家叫 Axiom Math 的创业公司说，他们自己开发的系统从 2 月份开始，已经投了 8 篇数学论文，其中 5 篇被期刊录用了。
说实话，乍一听觉得有点“科幻片”的味道。毕竟以前 AI 写数学，大多是靠“幻觉”——也就是瞎编一套看起来像那么回事的证明，但一检查就露馅。这次不一样，它似乎真的能搞出严谨的东西。
2. 到底解决了什么？
这次最让人眼热的，是关于“划分多项式倒数”的研究。这个领域本来就难啃，AI 不仅把 10 个核心猜想里 6 个给证出来了，还挖出了一个原命题的反例。
为什么这次不一样？
以前的 AI 模型，你问它一个数学问题，它用自然语言（也就是人话）给你编个证明，你根本没法确认它说的是不是真的，就像听人讲故事。
但 Axiom Math 搞了个新招数：Lean 形式化证明。
简单来说，就是先把问题翻译成计算机能看懂的、严丝合缝的“机器语言”。然后，每一个逻辑步骤都要经过独立的检测器过一遍，一步都卡壳不行。最后，人类数学家再出来把逻辑理顺、写成文章。
这就彻底堵死了“瞎编”的路子。虽然这过程挺累，需要人和机器来回打配合，但确实解决了“信任”这个最大的拦路虎。
3. 谁在干这事儿？
干这事儿的人，确实有点“非典型”。
25 岁的洪乐桐，中国人。
- 2001 年 在广州出生，数学天赋是从小就有，不是那种培训班练出来的。
- 17 岁 就进了麻省理工（MIT）。
- 3 年内 把数学和物理双学位拿下来了，本科期间发了 9 篇论文。
- 之后去了牛津读硕士，然后被斯坦福的双博士项目（法学 + 数学）录取。
按理说，这时候她的人生剧本应该是：在斯坦福读博，以后 maybe 去个顶尖研究所，发发顶刊。
但 2024 年秋天，她直接跟斯坦福说了“拜拜”，全职搞创业。这魄力，确实让人有点佩服，也有点担心。毕竟放弃已经到手的博士头衔去赌一个还没完全跑通的 AI 项目，风险可不小。
4. 钱和人都来了
不过，既然敢这么干，身后确实有底气。
- 团队配置：
- Shubho Sengupta：前 Meta AI 专家，联合创始人。
- Ken Ono：著名数学家，联合创始人（为了这个项目，直接从弗吉尼亚大学辞了终身教职）。
- 钱袋子：
- 不到一年时间，两轮融资下来，总共 2.64 亿美元（差不多 14 亿人民币）。
- 公司估值直接飙到 16 亿美元。
你看，资本嗅觉还是那么灵。只要沾上“可验证 AI"和“数学突破”这两个热点，钱就像不要钱一样往里砸。
5. 以后会咋样？
团队的目标显然不止于“当个 AI 数学家”。
除了之前在普特南数学竞赛（Putnam）拿满分，解决了困扰学界几十年的两个 Erdős 猜想 之外，他们最近已经把目光转向了 博弈论 和 经济学。
这背后的逻辑挺有意思：
如果能把“生成、形式化、验证”这套闭环推理能力，用到低风险、高精度的决策场景里（比如金融风控、策略制定），那价值就不仅仅是几篇论文了。
终极想法是搞一个具备 自我进化能力 的超级智能推理系统。
写在最后
看着这个进展，心情挺复杂的。
一方面，不得不承认这确实是个里程碑。AI 从“聊天陪玩”变成能解决硬骨头问题的工具，这一步迈得挺实。
另一方面，那种“一夜之间”似乎就搞定了人类数学家几十年的成果的感觉，又让人心里咯噔一下。毕竟，数学的直觉和美感，AI 真的能理解吗？还是说，它只是在玩一个极其复杂的概率游戏，碰巧蒙对了答案？
现在看起来，洪乐桐和她的团队把这条路铺得挺宽，但路该怎么走，还是得看时间。
