Papers With

← All papers
First page of The set of primes is supernatural: a Lean formalization of the statement of the conjecture

The set of primes is supernatural: a Lean formalization of the statement of the conjecture

A. Mayeux

cs.LO Aug 9, 2026 · v1
formalization number-theory logic
Read PDF arXiv abstract Code
TL;DR
Provides a complete, sorry-free Lean 4 formalization over Mathlib of the statement and supporting theory of the primes-are-supernatural conjecture.
Abstract
The paper Conjecture: the set of prime numbers is supernatural conjectures that no non-constant function built from the identity and constants by finitely many pointwise additions, multiplications, and exponentiations maps every positive integer to a prime. We give a complete Lean 4 formalization of that paper over Mathlib: every definition, example, remark, numbered result, and experimental table row has a machine-checked counterpart, with no \lcode{sorry}. The conjecture and similar generalizations are stated exactly, as named open problems. So stated, the conjecture becomes a precise target: an automated reasoning system can now attempt a kernel-checked proof.
Problem

A conjecture states that no non-constant function built from identity and constants via finitely many additions, multiplications, and exponentiations maps every positive integer to a prime. The goal is to state this precisely in a machine-checked form so it becomes a target for automated proof.

Approach

The paper formalizes the entire source paper in a single Lean 4 file (SPCL.lean) over Mathlib. Elevation structures become a type class, natural functions are encoded both via a word construction over operator letters and an inductive closure, with a proved equivalence. The central conjecture and its generalizations are stated as named plain Prop definitions with no proof or axiom attached, while proved cases (polynomials, exponential functions, Fermat's function) reproduce the source proofs.

Results

Every definition, example, remark, numbered result, and experimental table row of the source has a machine-checked Lean counterpart with no sorry. The file builds in about half a minute using only Mathlib's three standard classical axioms, and includes 89 experimental-table theorems plus Pratt primality certificates.