洪乐潼：AI for Math与数学形式化，将证明转化为Lean代码
洪乐潼分享AI for Math的愿景：用形式化工具（Lean）验证数学证明，并探讨数学的直觉与创造力。
嘉宾洪乐潼
节目简介
本期访谈00后创业者洪乐潼（Carina），她创办的Axiom公司致力于用AI辅助数学研究，刚完成2亿美元A轮融资。她讨论了数学既是发现也是创造的本质，如何将数学证明转化为Lean形式化语言，以及为何57岁终身教授小野肯辞职加入她的团队。
行业新闻
洪乐潼分享AI for Math的愿景：用形式化工具（Lean）验证数学证明，并探讨数学的直觉与创造力。
嘉宾洪乐潼
本期访谈00后创业者洪乐潼（Carina），她创办的Axiom公司致力于用AI辅助数学研究，刚完成2亿美元A轮融资。她讨论了数学既是发现也是创造的本质，如何将数学证明转化为Lean形式化语言，以及为何57岁终身教授小野肯辞职加入她的团队。