数学形式化 · 机器可验证证明

前沿数学证明已经长到人类审稿接近极限：动辄数百页，顶级期刊审几年仍可能漏错，望月新一的 IUT/ABC 猜想争议悬置十年就是标本——数学共同体内部竟无法就「证明是否成立」达成一致。形式化把证明写成计算机可逐步核验的代码，正确性不再依赖权威背书。Lean 的 mathlib 已经形式化了本科到部分研究前沿的数学，费马大定理形式化等大项目在推进；同时它给 AI 提供了一个答案绝对可判定的训练场——AlphaProof 类系统在形式化环境里做到了奥数级推理。攻破意味着数学获得工业级可信性，且人机协作可能改变数学生产本身的方式。

核心卡点是「形式化鸿沟」：把一页人类证明翻译成形式证明目前要花数十倍的工时，前沿数学中大量「显然」「同理可得」背后是机器暂时无法填补的直觉跳步。库的建设是超线性苦工——每形式化一个新领域都要先补齐它依赖的全部底层，而全球能干这活的人不足千人，激励机制（形式化不算学术成果）也压着供给。

Lean/mathlib 社区（Kevin Buzzard 领衔费马大定理形式化，Terence Tao 亦参与实践）、Google DeepMind（AlphaProof）、Coq/Isabelle 等老牌证明助手社区

这是六颗里入场门槛最低的：Lean 和 mathlib 全开源，本科数学水平就能提交第一个 PR，社区（Zulip）对新人极友好。路径：学 Lean → 认领 mathlib 里自己熟悉领域的缺口 → 参与大型形式化项目（如费马大定理）；若偏 AI，可切入自动形式化（autoformalization）——用大模型把自然语言数学翻译成 Lean，是当前最热的交叉缺口。