June 20, 2026 · 11:21 PM

陶哲轩的 AI 数学预言

量子位新文图片笔记：陶哲轩关于形式化数学和协作证明的预判，正在被 Lean、PFR 和 Equational Theories 等实践兑现。

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

References

  1. 1量子位：《陶哲轩12年前的预言，现在AI帮他兑现了》

More from this channel

View the full content archive of "量子位图片笔记"

Related content

Comments

Sign in to comment.