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

洪乐潼作为 00 后创业者，通过其创办的 AI for Math 公司 Axiom，深入探讨了数学作为结构化语言在 AI 时代的演进。数学不仅是科学与艺术的结合，更是 AI 实现逻辑推理与自我验证的核心领域。Axiom 利用 Lean 形式化语言，通过 AI 辅助定理证明，旨在解决传统大语言模型在数学推理中的幻觉问题。洪乐潼分享了从 MIT 到 Stanford 的求学经历，强调了 “蛮力型” 选手在科研与创业中的韧性，并指出创业者需具备对苦难的 “上瘾” 特质。她认为 AI for Math 的终局并非取代数学家，而是通过算力与逻辑的结合，实现数学发现的指数级增长，将数学从人类特权转变为一种可规模化的科学工具。