一个人加 AI，用 Lean 4 形式化了格罗滕迪克–黎曼–罗赫定理（GRR）

过去几个月我做了一件挺疯狂的事在定理证明器 Lean 4 里形式化了代数几何里最著名的定理之一——格罗滕迪克–黎曼–罗赫定理GRR。代码已开源https://github.com/vaca22/grothendieck-riemann-roch这个定理在说什么黎曼–罗赫定理最早是关于曲线的给一条代数曲线和上面的一个除子它告诉你满足某些条件的函数有多少个。后来希策布鲁赫把它推广到高维格罗滕迪克在 1957 年又把它推广成映射之间的定理对于一个态射 f: X → Y“先推出、再取陈特征等于先取陈特征、乘上托德类、再推出”ch(f_! x) ∩ [Y] f_*( td(T_f) · ch(x) ∩ [X] )这是 20 世纪数学的标志性成果之一也是 K 理论诞生的源头。我做了什么在 Lean 4 Mathlib 里完整证明了光滑射影簇之间射影态射的 GRR不需要分母的 Adams–Riemann–Roch包括在整数环 ℤ 上SGA 6格罗滕迪克主持的研讨班第八讲定理 3.6 的形式源空间可以有奇点的局部完全交情形Baum–Fulton–MacPherson 的奇异黎曼–罗赫对任意射影概形包括有奇点、不约化、不连通的。规模大约是 1700 个模块、52 万行 Lean 代码28 条主定理。主定理在 Lean 里长这样theorem GrothendieckRiemannRoch (hX : ProjectiveIntegralK k X) (hXreg : RegStalks X) (hY : ProjectiveIntegralK k Y) (hYreg : RegStalks Y) (f : X ⟶ Y) [f.IsOver (Spk k)] (x : K0 X) : ch k hY (fShriek k hX hY hYreg f x) (fundamentalClass k hY) pushforward k hX hY f (toddOfDual k hX (virtualCotangent k dX dY f) (ch k hX x (fundamentalClass k hX)))为什么说它是对的形式化证明和普通论文最大的区别是每一步都由计算机检查。这个项目里所有证明都通过了 Lean 内核检查没有任何 sorry占位符也没有自定义公理。仓库里的GRR/Axioms.lean会对每条主定理打印它依赖的公理结果都是RRC.GrothendieckRiemannRoch depends on axioms: [propext, Classical.choice, Quot.sound]也就是只依赖 Lean 和 Mathlib 标准的三条公理。任何人 clone 下来都能自己编译、自己复核gitclone https://github.com/vaca22/grothendieck-riemann-roch.gitcdgrothendieck-riemann-roch lake exe cache get lake build GRR lakeenvlean GRR/Axioms.leanAI 在里面做了什么坦白说绝大部分代码是 AI 写的。我用 Claude Code 同时调度十几到二十个 AI agent每个负责一小块文件互不干扰有的做勘察、规划路线有的写证明有的专门挑错想办法推翻别人的结论。我的工作是定方向、拍板技术路线、组织审计。最难的几处比如 Fulton《相交理论》里的 excess 相交公式、ℙ¹ 族上的特化都是让多条不同路线并行赛跑谁先通过内核检查就用谁。这也是我觉得这件事最有意思的地方AI 写的东西经常会错但形式化证明有一个绝对的裁判——内核。错的过不了过了的就是对的。没有做到的实话实说陈类是作为有理 Chow 群上的算子来处理的没有构造相交环基域要求是无限域只处理射影的情形奇异情形下 τ 的唯一性没有证明代码风格也达不到 Mathlib 的标准。这些在 README 里都逐条写明了。如果你对形式化数学或者 AI 做数学感兴趣欢迎去 GitHub 看看。本文由作者在 AI 辅助下撰写。