对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造的与被发现的
24岁的洪乐潼（Alex Hong）创办的Axiom（中文意取《数学天书中的证明》）刚刚完成估值16亿美元的A轮融资，吸引了57岁的终身教授小野健（Ken Ono）辞职加入。她在硅谷Facebook House接受了4小时访谈，讲述从广州奥数少年到MIT摩根奖、牛津神经科学、斯坦福数学与法学博士，再到辍学创立AI for Math公司的完整脉络。访谈涵盖Lean形式化语言如何把数学变成可验证的代码、Axiom的XProver如何以满分横扫普特南竞赛、为何她说自己是’蛮力型选手’而AI最大受益者正是蛮力型数学家、以及把数学家分为资源分配者与猜想家的未来图景。本文按主题整理，每个主题包含’新的变化’和’嘉宾观点与解释’两个维度，力求让未观看视频的读者快速理解核心内容与得出观点的原因。