137. 对洪乐潼的 4 小时访谈：AI for Math、把数学变成 Lean、数学天书的证明、直觉、被创造与被发现的

📌 一句话摘要

对话 00 后 AI for Math 创业公司 Axiom 创始人洪乐潼，深度探讨 AI 如何辅助数学证明与猜想、数学家直觉的本质、创业融资历程，以及数学作为「被创造」与「被发现」结构的哲学思考。

📝 详细摘要

本期播客深度访谈了年仅 24 岁的华人创业者洪乐潼（Carina），她是 AI for Math 公司 Axiom（公理）的创始人兼 CEO，公司近期完成了 2 亿美元 A 轮融资，估值 16 亿美元。访谈从洪乐潼的个人成长与数学启蒙开始，探讨了「数学是被创造还是被发现」的哲学命题，以及她作为「蛮力型」选手在 MIT 和牛津的学习经历。核心内容聚焦于她创办 Axiom 的愿景：利用 AI 系统辅助数学研究。她详细阐述了公司 AI 系统在 2025 年普特南数学竞赛中获得满分的历史性突破，并分析了 AI 证明与人类直觉证明的差异（如「一图解法」vs「数千行代码枚举」）。节目深入讨论了 AI for Math 的技术路径，包括形式化证明语言（如 Lean）、证明与猜想生成的互动系统、知识库构建，以及该能力向代码验证等领域的泛化潜力。此外，洪乐潼分享了吸引 57 岁终身教授小野肯（Ken Ono）加入团队的幕后故事，并坦诚回顾了作为年轻女性 CEO 的融资挑战、团队文化建设以及对 AI 与数学共同进化的未来展望。

💡 主要观点

- AI 在数学证明上展现「蛮力型」与「直觉型」互补能力 洪乐潼的 AI 系统在普特南竞赛中，对同一道题给出了与人类「一图解法」完全不同的「数千行代码枚举」证明，体现了 AI 处理复杂问题的独特路径，与人类数学家的天赋形成互补而非替代。

AI for Math 的核心是构建证明与猜想生成的互动系统 Axiom 不仅训练 AI 进行形式化证明，还致力于构建能提出新猜想的系统。两者形成闭环：证明验证猜想的正确性，猜想为证明提供新的方向，同时需要庞大的形式化数学知识库作为支撑。

数学证明能力可泛化至代码验证等关键领域 访谈中提到一个关键洞察（aha moment）：擅长数学定理证明的 AI prover，同样展现出强大的代码验证能力。这揭示了数学形式化逻辑与软件验证在底层的一致性，为 AI 在关键领域（如芯片验证）的应用开辟了道路。

创业者的「自由注意力」是产生战略洞察的关键 洪乐潼区分了「被框架的注意力」与「自由注意力」，认为后者是区分普通执行者与卓越战略决策者的关键。她怀念童年时漫无目的思考数学的时光，并认为保护这种「自由注意力」对保持创新活力至关重要。

数学是介于「被发现」结构与「被创造」公理体系之间的艺术 洪乐潼认为，数学结构本身可能客观存在（被发现），但人类选择不同的公理体系去描述和搭建它，则是一个充满创造性和艺术性的过程。数学家社群通过证明达成共识，推动数学理论螺旋式发展。

💬 文章金句

- 我们公司在这个普特南大学生数学竞赛中，就是这个 AI prover 拿了满分。然后是人类历史上有五个满分，过去的 98 年... 这是第六个满分，是一个 AI 拿到的。

• 第二个我觉得有一个我们的 aha moment，其实是就是我们发现这个数学的定理证明的很好的一个 AI prover，能够转化到它很强的代码验证能力。
• 但是就是后面这一个自由注意力，其实是能够区分一个平均的一个创业者和一个很很好的一个很有策略性和决策性的一个创业者的一个区别。
• 他们其实一个想法就是随着 AI 的进步，人类数学家会学习在不同的抽象层面上进行逻辑推理。
• 我们希望能够执行速度很快，我们也希望探索商业模式的这些从一个技术的角度去探索，从技术和好奇心的角度去探索商业模式。

📊 文章信息

AI 初评：94

来源：张小珺Jùn｜商业访谈录

作者：张小珺

分类：人工智能

语言：中文

阅读时间：368 分钟

字数：91993

标签： AI for Math, 自动定理证明, 形式化验证, 数学直觉, AI 创业

收听完整播客