137. 对洪乐潼的4小时访谈:AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的
张小珺对 24 岁 Axiom 创始人洪乐潼的 4 小时长访谈。00 后华人女孩、MIT 摩根奖得主、 斯坦福数学博士辍学、A 轮 16 亿美元。访谈把 AI for Math 的来龙去脉讲透——从 1960s ATP 到 2024 年 DeepMind AlphaProof,再到 2025/12 Axiom 拿下 Putnam 满分 98.93%; 也讲透了洪乐潼的创业心智:蛮力型选手、对苦难上瘾、bet system not model、 把自己定义成 "research scientist intern" 而非 CEO。