EP05 对话Lean Prover主创Jeremy｜这是我们的数学：AI、验证与数学的未来 Avigad

Jeremy Avigad 是卡内基梅隆大学哲学系和数学科学系的教授。他是将人工智能应用于数学领域的先驱，也是 Lean Theorem Prover的主创。目前，他担任卡内基梅隆大学 Hoskinson 形式数学中心主任、逻辑与数学哲学讲席教授，以及美国国家科学基金会（NSF）新成立的"计算机辅助数学推理研究所"主任。

时间轴（Outline）:

00:00 - 精彩预告

01:04 - 独白

02:50 - AI 应用于数学的历史图景

07:28 - 形式化与计算机辅助证明

11:56 - Lean 项目的诞生

21:21 - Lean 蓝图、基于 Lean 的模型训练、在智能体系统中使用 Lean

29:48 - 如何让 AI 真正对数学家有用

32:46 - AI 如何改变数学

36:29 - "这是我们的数学，是我们自己在做数学"

43:04 - 人机协作中的验证鸿沟

47:46 - 数学教育的未来

52:23 - 资本、初创企业与数学家生态

1:01:08 - 预测

参考文献:

• Jeremy的个人主页: www.andrew.cmu.edu

• The Lean Theorem Prover: lean-lang.org

• Lean 项目列表: leanprover-community.github.io