5 papers · 1 filter
Projective blowups: a formal and multicentered proof
A. Mayeux
We give a machine-checked proof, in Lean 4, of the universal property of multicentered blowups: given a finite family of closed subschemes of a scheme , presented on each ch…
The set of primes is supernatural: a Lean formalization of the statement of the conjecture
A. Mayeux
The paper \emph{Conjecture: the set of prime numbers is supernatural} conjectures that no non-constant function built from the identity and constants by finitely many pointwise add…
Formalizing multi-graded Brenner-Schröer Proj schemes and dilatations of rings in Lean4
Arnaud Mayeux, Jujian Zhang
We present a detailed formalization in Lean4 of some multigraded algebraic geometry constructions, focusing on the Brenner--Schröer Proj construction and algebraic dilatations of r…
Formalizing all indexed mathematics as a benchmark for general reasoning, with the example of implementing dilatations of categories
A. Mayeux
Formal rigor distinguishes mathematics from other disciplines, in the sense that mathematical statements are derived from explicit axioms by logically verifiable steps. Interactive…
Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
A. Mayeux
Mathematical knowledge is split between bibliographic databases (e.g., MathSciNet, zbMATH Open) and formal proof libraries (e.g., Lean's mathlib), preventing unified access to publ…