How to Formalize All of Mathematics
摘要
Jeremy Avigad、Kevin Buzzard、Johan Commelin 等七位作者在 Kevin Buzzard 博客发文《How to Formalize All of Mathematics》，回应近期自动形式化全部数学文献的提案。文章指出形式数学与 informal 数学面临平行的问题，核心在于优先产出时速度、规模与理解之间的权衡，全文主要围绕这一权衡展开。
摘要由模型根据原文撰写，以原文为准。
正文 · 原文
Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash and Adam Topaz have written a blog post over on Kevin Buzzard’s blog entitled “How to Formalize All of Mathematics”, regarding recent proposals to automatically formalize the entirety of the mathematical literature. The issues regarding formal mathematics are parallel to those regarding informal mathematics, in particular the tradeoff between speed, scale, and understanding when one prioritizes the production of output over all other desiderata, and the blog post is largely focused on this tradeoff.
注意转载授权 · 阅读原文
来源：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/.