如何形式化全部数学：Jeremy Avigad、Kevin Buzzard 等谈自动形式化整部数学文献的提案
摘要
Jeremy Avigad、Kevin Buzzard、Johan Commelin 等七位作者在 Kevin Buzzard 博客发文《How to Formalize All of Mathematics》，回应近期自动形式化全部数学文献的提案。文章指出形式数学与 informal 数学面临平行的问题，核心在于优先产出时速度、规模与理解之间的权衡，全文主要围绕这一权衡展开。
摘要由模型根据原文撰写，以原文为准。
正文 · AI 翻译
Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash 和 Adam Topaz 在 Kevin Buzzard 的博客上写了一篇题为“如何形式化全部数学”的博文，讨论近期关于自动形式化全部数学文献的提议。形式数学所涉及的问题与非形式数学的问题相平行，特别是当人们将产出置于所有其他期望之上时，速度、规模与理解之间的权衡，而这篇博文主要聚焦于这一权衡。
注意转载授权 · 阅读原文。中文正文为 AI 翻译，请以原文为准。
来源：Terence Tao 博客 · terrytao.wordpress.com
引用原文
Terence Tao. How to Formalize All of Mathematics[EB/OL]. (2026-10-16)[访问日期]. https://terrytao.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/.