{"id":"arxiv/2609.28489","url":"https://arxiv.org/abs/2609.28489","tags":["math.AG","cs.LO"],"score":0,"title":"Projective blowups: a formal and multicentered proof","domain":"math.AG","source":"arxiv","authors":["A. Mayeux"],"reviews":0,"subject":"math.AG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-13","reactions":{}}