射影爆破：一种形式化与多中心的证明
Projective blowups: a formal and multicentered proof
A. Mayeux
AI 速读 基于摘要
作者报告在 Lean 4 中机器验证了多中心爆破的泛性质，并称这是任意定理证明器中首次对（单中心或多中心）爆破的形式化。
math.AG · cs.LO
查看原文摘要
We give a machine-checked proof, in Lean 4, of the universal property of multi- centered blowups: given a finite family Z of closed subschemes of a scheme X, presented on each chart by ideals, there is a scheme BlZ X over X, terminal among X-schemes on which every member of the family becomes an effective Cartier divisor. To the best of our knowledge this is the first formalisation of blowups, single- or multicentered, in any theorem prover. The proof is organised around the universal property of the multicentered dilatation of a ring. The comparison isomorphisms on overlaps, the cocycle identity, and the independence of the chosen presentation are obtained from the uniqueness part of this universal property. We give the exact theorem statement as formalized, the proof architecture, and the main new mathematical ingredients, together with the corresponding Lean code.