发表机构
University of Wisconsin-Madison（威斯康星大学麦迪逊分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文在 Lean 4 中形式化证明了多中心 blowing up 的泛性质，通过局部建立环的膨胀并利用唯一性推导全局构造，首次在定理证明器中实现 blowing up 的形式化。
AI 中文摘要
我们给出了一个在 Lean 4 中机器检查的关于多中心 blowing up 的泛性质的证明：给定一个概形 $X$ 的闭子概形的有限族 $Z$，在每个图表上由理想呈现，存在一个 $X$ 上的概形 $\Bl_Z X$，它是所有使得该族中每个成员成为有效 Cartier 除子的 $X$-概形中的终对象。据我们所知，这是在任何定理证明器中首次对 blowing up（单中心或多中心）的形式化。该证明围绕环的多中心膨胀的泛性质组织：即一个有限理想族由非零因子生成的初始代数。膨胀的存在性和唯一性在仿射图表上局部建立，并且构造的每一步——沿开浸入的基变换、重叠上的比较同构、三重重叠映射、余循环恒等式以及所选呈现的独立性——都仅通过唯一性从该单一局部性质推导出来。我们给出了形式化的精确定理陈述、证明架构和主要的新数学成分，以及相应的 Lean 代码。
英文摘要
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.
