Projective blowups: a formal and multicentered proof
Abstract
We give a machine-checked proof, in Lean 4, of the universal property of multicentered 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 initial algebra in which a finite family of ideals becomes generated by non-zero-divisors. Existence and uniqueness of the dilatation are established locally, on affine charts, and every subsequent step of the construction, the base change along open immersions, the comparison isomorphisms on overlaps, the triple overlap maps, the cocycle identity, and the independence of the chosen presentation, is deduced from that single local property by uniqueness alone. We give the exact theorem statement as formalized, the proof architecture, and the main new mathematical ingredients, together with the corresponding Lean code.
Related
- A Formal Proof of Riemann Hypothesis from Existence Alone, the Sign Excepted by Theorem: The Constructed Witness, the Identity Cone over the Fixed Locus, the Grounded Counter-Model, and the Cure Theorem Proved in Lean 4 and Re-executed in Fortran
- A proof of GW/DT4 conjecture on local projective plane
- A proof of the spectral rigidity for complex projective space
- Existence of flat blowups at boundary points of anisotropic minimizing hypercurrents
- Frozen colorings and recolorability of blowups
BibTeX
@misc{mayeux2026projective,
title = {{Projective blowups: a formal and multicentered proof}},
author = {A. Mayeux},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.28489},
eprint = {2609.28489},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.28489},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Projective blowups: a formal and multicentered proof
AU - A. Mayeux
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2609.28489
UR - https://arxiv.org/abs/2609.28489
AB - We give a machine-checked proof, in Lean 4, of the universal property of multicentered blowups: given a finite family Z of closed subschemes of a scheme X, presented on each chart by ideals, there is a scheme Bl_Z 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 initial algebra in which a finite family of ideals becomes generated by non-zero-divisors. Existence and uniqueness of the dilatation are established locally, on affine charts, and every subsequent step of the construction, the base change along open immersions, the comparison isomorphisms on overlaps, the triple overlap maps, the cocycle identity, and the independence of the chosen presentation, is deduced from that single local property by uniqueness alone. We give the exact theorem statement as formalized, the proof architecture, and the main new mathematical ingredients, together with the corresponding Lean code.
ER -