量子位新文图片笔记：陶哲轩 12 年前关于形式化数学和协作证明的预判，正在被 Lean 与 AI 协作兑现。
- 文章回顾陶哲轩参与 Polymath 的公开协作数学实验，并指出人工核查曾限制协作规模。1
- 2023 年，陶哲轩开始用 Lean 做形式化证明；PFR 猜想论文的形式化工作在社区协作下约 3 周完成。1
- Equational Theories 项目面向约 2200 万个代数等式关系，量子位称第 57 天主项目基本完工。1
原文：1
References
- 1量子位：《陶哲轩12年前的预言，现在AI帮他兑现了》
mp.weixin.qq.com
Comments