9 papers
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…
The mechanization of science illustrated by the Lean formalization of the multi-graded Proj construction
Arnaud Mayeux, Jujian Zhang
We formalize the multi-graded Proj construction in Lean4, illustrating mechanized mathematics and formalization.
Algebraic magnetism invariants of a double scalar action on the projective plane
Arnaud Mayeux
This document is an expanded version of the notes from a talk at the \textit{Arithmetic and Algebraic Geometry Week} conference, which took place in Iasi in September 2025. In this…
Algebraic Magnetism Invariants of Self-Actions of Diagonalizable Monoid Schemes
Arnaud Mayeux
We provide a method to compute the pure magnets of the action of a diagonalizable monoid scheme on itself. This is described in terms of minimal generators of the sharp monoid obta…
Conjecture: the set of prime numbers is supernatural
Arnaud Mayeux
Prime numbers are fascinating by the way they appear in the set of natural numbers. Despite several results enlighting us about their repartition, the set of prime numbers is often…