对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明

00后华人女孩洪乐潼（Carina）创办的 AI for Math 公司 Axiom（公理）刚完成2亿美元A轮融资，估值16亿美金，这是她首次接受中文访谈。她探索的方向是 AI for Math，包括把数学变成 Lean。57岁美国终身教授小野肯（Ken Ono）辞职加入她的团队。