一份根据《商业访谈录》对Axiom创始人洪乐潼（Carina）专访内容整理的分享备忘Memo：

商业访谈录备忘：AI for Math与数学少女的探索之旅

嘉宾背景信息

• 姓名：洪乐潼（Carina Hong），00后华人创业者。

• 身份：Axiom（公理）公司创始人兼CEO。

• 公司概况：致力于AI for Math领域，近期完成2亿美元A轮融资，估值达16亿美元。

• 学术经历：本科就读于MIT（数学与物理），硕士就读于牛津（计算神经科学），博士就读于斯坦福（数学与法学）。

一、 数学的本质：在艺术与科学之间搭建公理

• 数学是契约与结构：数学并非简单的解题，而是一套文明体系。数学家们达成“契约”，在一套公理系统上不断向上搭建理论，它介于艺术与科学之间。

• 发现还是创造？：数学发现的过程需要共识。证明不仅是逻辑的严丝合缝，更是一种影响力。只有当证明被接受，数学发现才真正成为文明的一部分。

• 关于美感的直觉：洪乐潼认为数学最美的时刻在于跨领域的交集，例如代数表达式与几何物体的联系（如模形式椭圆曲线定理）。

二、 个人成长：从“蛮力型选手”到长期主义者

• 拒绝零和游戏：在数学竞赛的压力下，她意识到自己并非“天赋型选手”，而是依靠勤勉的“蛮力型选手”。她通过学习高等数学来跳出竞赛的零和博弈，转向正和的知识探索。

• 自由注意力（Free Attention）：区分平庸与卓越创业者的关键在于能否保护好“自由注意力”。这种非线性、发散性的思维状态是产生灵感和策略性决策的土壤。

• 对苦难的上瘾：创业者往往是对苦难（Suffering）上瘾的人。洪乐潼在MIT学到的重要品质是毅力——在极端压力下保持内核的坚持。

三、 AI for Math：人工智能在逻辑高地的突破

• 大力出奇迹的AI：Axiom Prover在普特南数学竞赛中获得满分，展现了AI通过枚举、分类讨论等“蛮力”手段解决人类天才型创造力问题的可能性。

• 形式化证明（Lean语言）：将数学语言代码化。Lean不仅是编程语言，更具备自我验证能力。它将数学逻辑从自然语言的松散中解放出来，实现严丝合缝的验证。

• 核心技术三角：

  • Proving（证明）：逻辑推导与验证。

  • Conjecturing（猜想）：提出有意义的数学问题，这是目前的难点。

  • Auto-formalization（自动形式化）：将人类浩如烟海的数学文献转化为机器可理解的代码，这是通往超级智能的桥梁。

四、 Axiom的愿景：深科技（Deep Tech）的“SpaceX”

• 定位深科技而非单纯的模型公司：Axiom被视为深科技领域的SpaceX，具有极高的工程壁垒和长研发周期。

• 首个商业落地：验证（Verification）：

  • 软件与芯片验证：目前传统验证手段耗时耗力。AI可以在编写程序的同时进行数学层面的验证，确保代码百分之百正确。

  • Math is Code, Code is Math：任何能定义的都能被证明，任何能表达的都能被执行。

• 指数级增长的发现：AI将使数学从匮乏走向丰富，带来数学发现的爆炸式增长。人类数学家将转型为“资源分配者”，利用直觉决定算力的投入方向。

五、 启发洞察：好奇心驱动的未来

• 递归式自我提升（Recursive Self-improvement）：当AI具备了自我验证和提出新猜想的能力，智能将进入加速循环。

• 跨学科的连接力：法学的严谨、物理的逻辑与AI的算力在数学这一“现实世界的沙盒”中汇聚。

• 学徒心态：洪乐潼将自己定义为“学徒”。她认为人类的好奇心是无法被压制的基本动力，即使AI解决了所有问题，人类依然会因为想要看懂证明而产生新的好奇。

核心金句： “我们相信任何能定义的都能被证明，任何能表达的都能被执行。” “解决一个有意义的失败，比很多个肤浅的成功来得更有价值。”