# 数学从此永远改变——Kevin Hartnett

- 原标题：Mathematics Just Changed Forever — Kevin Hartnett
- 类型：博客
- 来源：YouTube
- 发布时间：2026-10-26
- 首次精选：2026-10-27 10:05
- 分级：值得看
- 学习层级：入门
- 主题：[ai-mathematics-proofs](<https://oplearnx.com/md/topics/ai-mathematics-proofs.md>)（第 3 位）
- 原文链接：[https://youtube.com/watch?v=IRJDwtAreB4](<https://youtube.com/watch?v=IRJDwtAreB4>)
- 本站页面：[https://oplearnx.com/resources/pk\_682478313c17](<https://oplearnx.com/resources/pk_682478313c17>)

## 摘要

这是一个围绕 Kevin Hartnett 著作《The Proof in the Code》制作的纪录片式访谈视频。内容从 1998 年 Thomas Hales 计算机辅助证明开普勒猜想、Annals of Mathematics 无法判定其正确性讲起，讲述 Lean 从微软研究院的副项目发展为数学界用于校验证明的系统，并采访了 Lean 创建者 Leonardo de Moura、Jeremy Avigad、Kevin Buzzard 等人。后半部分转向 AI，涉及 AlphaProof、自然语言奥赛证明、自动形式化，以及“形式化鸿沟”这一概念。

---
来源：LearnMap · 学径（https://oplearnx.com）