「数学自动形式化计划」启动:称距把全部已知数学转成形式化代码仅差三个数量级

i_dg23 · x · 2026-09-11

jdlichtman 发布文章《The MAP: Mathematics Autoformalization Project》,主张把人类全部已知数学翻译成形式化代码,并将其类比为一部「数学版人类基因组计划」或当代的 AlphaFold。

作者认为以 Anthropic 9 月 4 日在数学能力上的突破为标志,这项工程已具备可行性,当前距完成全部数学的形式化只差约三个数量级的进展。这是一条关于 AI 加速数学研究走向的判断性观点。