58
0Jeremy 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
