阅读材料：数学家与人工智能
第一学时提到的几件事，来龙去脉都在这里。
一陶哲轩的看法与做法
陶哲轩 Terence Tao
顶尖数学家里，较早亲自动手把人工智能和机器证明用进研究的一位。
先认识 Lean：会检查证明的软件
三年时间线
- “三个都大于 1 的数，和至少是 3”，一笔带过
- 去 Mathlib 找对应的引理
- 数字 3 是整数还是实数，逐处标明
他的发现：证明里难的部分写进 Lean 反而顺利，简单的部分却很费工夫。
他怎么看人工智能
熟路强，前沿弱
资料多、路子熟的问题表现很好，到了资料少的研究前沿容易失手。
最有成效的是查文献
近期的好用法，未必是攻最难的题，而是找出相关的已有文献。
回到理解
少看“解决了多少公开问题”，重新重视人对数学的理解。
Quanta Magazine，2026-06-08；陶哲轩 Mathstodon，2025-10-16；The Atlantic，2026-09；Leslie Ann Goldberg，Mathematics and AI；陶哲轩，arXiv:2608.16753。
二奥数三年：从银牌到满分
dots-note-3.0 怎么做到的
和我们要求学生的“做完要检查”是同一个道理。
这些数字可信到什么程度
官方评阅比团队自报可信得多；证明公开、能用 Lean 复核的最站得住。
dots 团队 IMO 2026 满分说明；China Daily，Chinese AI model sets record with perfect score，2026-07-22；IMO 官网 2026 年成绩页。
三解决数学难题的新闻
OpenAI Astra：十个问题，八个方向
2026 年 8 月公布，附长篇论文，有的问题悬置了几十年。
非 sofic 群
给出明确反例，并用 Lean 4 机器验证。
Connes 刚性猜想
构造出例子，给出否定回答。
高维球堆积
确定 Cohn–Elkies 方法的极限强度，得到更好的上界。
核验进度
这批结果由 OpenAI 自己公布。《新科学家》的报道指出，借用了多少前人工作没有说清。
厄尔多斯问题：上千道题，人机一起清点
核验
用 Lean 核验已有的证明
计算
算出相关的整数数列
补全
补上证明中缺失的步骤
扫描
找出题目写错的、容易拿下的
OpenAI，Ten advances in mathematics and theoretical computer science，2026-08；New Scientist，2026-08-03；陶哲轩 Mathstodon，2025-11-30。
四数学家的不同声音
陶哲轩设想人机分工：机器做大量容易的小问题，证明交给 Lean 检查，人负责最难的部分和方向。
成果借用了多少前人工作没讲清；已出现无人从头到尾细读过的机器证明，原因是还没人有时间细看。
不能只拿“解决了多少难题”衡量数学。牛津大学的 Goldberg 也整理了这些讨论与自己的用法。
Quanta Magazine，2026-06-08；New Scientist，2026-08-03；The Atlantic，2026-09；Leslie Ann Goldberg，Mathematics and AI。
五未来方向与数学教育
2014 → 2024：一个设想的十年
2014 年陶哲轩设想：将来几百位数学家合作一个项目，论文由计算机检查而非人审稿。同台数学家觉得不可思议，十年后它已部分成为现实。
人机怎样分工
- 提出猜想
- 尝试证明
- 处理大量容易的小问题
- 检查每一步对不对
- 通过即无逻辑漏洞
- 提出值得研究的问题
- 判断方向，攻最难的部分
- 真正理解得到的结果
对初中课堂意味着什么
检验不能省
“代回原题检验”就是最朴素的验证。
学会判断
哪个结论有依据，哪一步站不住。
理解不能外包
懂没懂，要由学生自己讲出来、写出来。
Quanta Magazine，2026-06-08；The Atlantic，2026-09；陶哲轩，Mathematics in the age of AI，arXiv:2608.16753。
附原文链接
链接需要联网打开，部分网站在国内访问可能较慢。