怎样把全部数学形式化 — Hacker News 中文摘要

📋 概述

这是一篇由 Jeremy Avigad、Kevin Buzzard、Johan Commelin、Rémy Degenne、Kim Morrison、Oliver Nash、Adam Topaz 联名的客座文章，回应 OpenAI 上次发布后出现的把全部数学尽快形式化的呼声。他们同情这个目标，但对尽快做完的呼吁深感担忧：没人使用的形式化产物几乎没有价值，Math, Inc. 曾劫持球填充项目、Anthropic 用 11 天写出 1300 万行代码验证费马大定理，这些成果都很惊人，但留下来能继续做数学的价值有限。作者提出 Mathlib、Formal Conjectures 与 Annals Challenge 等他们认为正确的做法。