如何形式化全部数学：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 的博客上写了一篇题为“如何形式化全部数学”的博文，讨论近期关于自动形式化全部数学文献的提议。形式数学所涉及的问题与非形式数学的问题相平行，特别是当人们将产出置于所有其他期望之上时，速度、规模与理解之间的权衡，而这篇博文主要聚焦于这一权衡。

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.

注意转载授权 · 阅读原文。中文正文为 AI 翻译，请以原文为准。

注意转载授权 · 阅读原文

如何形式化全部数学：Jeremy Avigad、Kevin Buzzard 等谈自动形式化整部数学文献的提案

摘要

正文 · 双语对照

引用原文