# 数学家提出如何用 AI 高质量地形式化全部数学

> 原标题：How to Formalize All of Mathematics

- 来源：Hacker News 首页
- 发布时间：2026-10-16T14:01:53.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/xkf3xqvff7o3qe9c7od0cllym
- 原文：https://xenaproject.wordpress.com/2026/10/16/how-to-formalize-all-of-mathematics/

## 摘要

Jeremy Avigad、Kevin Buzzard 等数学家提出，AI 辅助的大规模数学形式化应以可理解、可复用的高质量形式库为目标，并认为三年内、甚至更早可能覆盖大部分数学。