Showing cs.LOShow all
3 papers · 1 filter
cs.LO2026
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…
cs.LO2026
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…
cs.LO2025
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.