From the 1 of 8 linked papers with an AI index.
8 papers
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…
Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge
A. Mayeux
The paper proposes a relational bridge database that links bibliographic metadata with formal proof libraries and introduces a formalization score to estimate how much of a publica…
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…
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…
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…
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.