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

📌 一句话摘要 对话 00 后 AI for Math 创业公司 Axiom 创始人洪乐潼，深度探讨 AI 如何辅助数学证明与猜想、数学家直觉的本质、创业融资历程，以及数学作为「被创造」与「被发现」结构的哲学思考。 📝 详细摘要 本期播客深度访谈了年仅 24 岁的华人创业者洪乐潼（Carina）