The Set of Primes is Supernatural: A Lean Formalization

Summary (Overview)

• This paper presents a complete formalization in Lean 4 of the mathematical paper "[3]" (titled "The Set of Primes is Supernatural") using the Mathlib library.
• The formalization covers every definition, example, remark, proposition, and experimental table row from the original paper, with no sorry or unproved axioms.
• The central conjecture (Conjecture 2.1) is stated as a named Prop without proof, deliberately preserving its open status.
• The formalization extends the original work by implementing Remark 3.4's suggested extensions: Knuth arrows, factorial, and truncated subtraction in a single inductive class.
• All 89 experimental table rows are proved, with the largest primality checks handled by kernel-verified Lucas certificates.

Introduction and Theoretical Foundation

Background

The original paper [3] concerns natural functions on positive integers (denoted $\mathbb{I}$ or $\mathbb{N}^+$): functions built from the identity and constant functions using finitely many applications of pointwise addition ($+$), multiplication ($\times$), and exponentiation ($\wedge$). The central conjecture states:

Conjecture 2.1 ([3]): No non-constant natural function maps every positive integer to a prime.

The paper develops a theory of elevation structures — algebraic structures axiomatizing the compatibilities between $+$, $\times$, and $\wedge$ — and proves several partial results toward the conjecture.

Elevation Structures

An elevation structure is a 4-tuple $(E, +, \times, \wedge)$ where $E$ is a set and all three operations are binary maps $E \times E \to E$ satisfying seven axioms:

(i) $a + b = b + a$
(ii) $a + (b + c) = (a + b) + c$
(iii) $b \times a = a \times b$
(iv) $a \times (b \times c) = (a \times b) \times c$
(v) $a \times (b + c) = a \times b + a \times c$
(vi) $(a \wedge b) \times (a \wedge c) = a \wedge (b + c)$
(vii) $(a \wedge b) \wedge c = a \wedge (b \times c)$

Crucially, $\wedge$ itself need be neither commutative nor associative. The convention fixes right-associativity: $a_1 \wedge a_2 \wedge \cdots \wedge a_n$ means $a_1 \wedge (a_2 \wedge (\cdots \wedge a_n))$.

Key Examples

1. $(\mathbb{I}, +, \times, \wedge)$ with $\wedge$ as ordinary exponentiation is an elevation structure.
2. $(\mathcal{F}, +, \times, \wedge)$ where $\mathcal{F}$ is the set of functions $\mathbb{I} \to \mathbb{I}$ with pointwise operations is an elevation structure. The evaluation map $E_a : \mathcal{F} \to \mathbb{I}$, $f \mapsto f(a)$, is a morphism.

Natural Functions

Let $\mathcal{F}_s \subset \mathcal{F}$ consist of the identity map and all constant maps. For $P \subseteq \mathcal{F}$, define $A_+(P)$ (resp. $A_\times(P)$, $A_\wedge(P)$) as $P$ together with all $g+h$ (resp. $g \times h$, $g \wedge h$) for $g, h \in P$. Writing $\Sigma$ for the set of finite words in the alphabet $\{A_+, A_\times, A_\wedge\}$, the set of natural functions is:

$$\mathcal{F}_{\text{Natural}} = \bigcup_{\sigma \in \Sigma} \sigma(\mathcal{F}_s)$$

The length of a natural function $f$ is the least length of a word $\sigma \in \Sigma$ with $f \in \sigma(\mathcal{F}_s)$.

Formalization Approach

Two Encodings of Natural Functions

The formalization uses two equivalent encodings:

First encoding (word machinery): An inductive type OpLetter with constructors plus, mul, elev. Words are lists of letters acting on sets of functions by composition. FNatural is the union over all words.

inductive OpLetter : Type
| plus | mul | elev

def OpLetter.apply : OpLetter → Set (N+ → N+) → Set (N+ → N+) := ...

abbrev Word := List OpLetter

def Word.apply (σ : Word) (P : Set (N+ → N+)) : Set (N+ → N+) := ...

def FNatural : Set (N+ → N+) := ∪ σ : Word, Word.apply σ Fs

Second encoding (inductive predicate): A direct inductive predicate IsNatural on functions:

inductive IsNatural : (N+ → N+) → Prop
| id : IsNatural (fun n => n)
| const (c : N+) : IsNatural (fun _ => c)
| add {f g} (hf : IsNatural f) (hg : IsNatural g) : IsNatural (fun n => f n + g n)
| mul {f g} (hf : IsNatural f) (hg : IsNatural g) : IsNatural (fun n => f n * g n)
| elev {f g} (hf : IsNatural f) (hg : IsNatural g) : IsNatural (fun n => (f n) ^ (g n : N))

The two encodings are proved equivalent, giving for free the induction principle the paper obtains from the word definition.

Category Formalization

The paper's sentence "we obtain a category" is fully formalized: identity, composition, and the three category laws hold definitionally (rfl). The category is also registered as an instance of Mathlib's Category class.

Key Theorems Formalized

Proposition 1.6: Natural Functions are Constant or Strictly Increasing

def ConstOrStrictMono (f : N+ → N+) : Prop := (∃ c, ∀ n, f n = c) ∨ StrictMono f

theorem isNatural_constOrStrictMono {f : N+ → N+} (hf : IsNatural f) : ConstOrStrictMono f

The proof follows the paper's structure via three closure lemmas (Lemmas 1.8–1.10), with the elevation case carrying the base-1 exception:

theorem lemma_1_10 {h : N+ → N+} (c : N+) (hh : StrictMono h) :
  (1 < c → StrictMono (fun n => c ^ (h n : N))) ∧
  (c = 1 → ∀ n, c ^ (h n : N) = 1)

Remark 1.11: Why the Domain is Positive Integers

On $\mathbb{N}$, the map $n \mapsto n^n$ is neither constant nor strictly increasing ($0^0 = 1^1 = 1$ while $2^2 = 4$). Both halves are formalized, showing why the theory uses $\mathbb{I}$ not $\mathbb{N}$.

Proposition 2.2: Proved Cases of the Conjecture

Case (i) — Polynomial functions: Uses the fact that $x - y \mid q(x) - q(y)$ for integer polynomials to show that for a prime $p \mid f(n)$, we get $p \mid f(n+p)$ with $1 < f(n) < f(n+p)$, so $p$ is a proper divisor.

Case (ii) — Functions of form $f(n) = a^n + b$: Uses Fermat's little theorem to handle the case where $p \nmid a$.

Case (iii) — Fermat's function: Euler's factorization of the fifth Fermat number is kernel-checked:

theorem fermatFn_five_eq : (fermatFn 5 : N) = 641 * 6700417 := by decide

Proposition 3.1: Consequences of the Conjecture

The paper asserts that if $f$ is natural and $k \in \mathbb{I}$, then $g(n) := f(n+k)$ is natural. This requires an auxiliary lemma:

theorem IsNatural.comp {f g : N+ → N+} (hf : IsNatural f) (hg : IsNatural g) :
  IsNatural (f ∘ g)

theorem isNatural_shift (k : N+) : IsNatural (fun n : N+ => n + k)

Corollary 3.2: Infinitely Many Composite Fermat Numbers

Formalized as a conditional theorem:

theorem corollary_3_2 (hconj : Conjecture_2_1) :
  {n : N+ | ¬ Nat.Prime (fermatFn n : N)}.Infinite

The Extended Class (Remark 3.4)

The formalization implements a substantial extension combining three new features:

1. Knuth arrows whose level is itself a function in the class
2. Factorial
3. Truncated subtraction, admitted only under pointwise hypothesis $g(n) < f(n)$

Mathlib's hyperoperation indexes the hierarchy: index 0 = successor, 1 = addition, 2 = multiplication, 3 = exponentiation (the paper's elevation $\wedge$), 4 = tetration, etc. Knuth's arrows begin at exponentiation, so $j$ arrows correspond to index $j+2$:

$$a \uparrow^j b = \text{hyperoperation}(j+2) a b \quad (j \geq 1)$$

inductive IsNaturalKnuthFactorialSub : (N+ → N+) → Prop
| id | const | add | mul
| knuth {f g h} (hf : IsNaturalKnuthFactorialSub f) (hg : ...) (hh : ...) :
    IsNaturalKnuthFactorialSub (fun n =>
      ⟨hyperoperation ((g n : N) + 2) (f n) (h n), hyperoperation_pos_of_three_le ...⟩)
| fact {f} (hf : ...) :
    IsNaturalKnuthFactorialSub (fun n => ⟨(f n : N).factorial, ...⟩)
| sub {f g} (hf : ...) (hg : ...) (hlt : ∀ n, (g n : N) < (f n : N)) :
    IsNaturalKnuthFactorialSub (fun n => ⟨(f n : N) - (g n : N), ...⟩)

The embedding theorem IsNatural.toKnuthFactorialSub verifies that the extension genuinely extends the original class.

The Experimental Tables (§4)

All 89 table rows are formalized as theorems. Each row states that values are prime at each earlier point and not prime at the reported point, proved by norm_num.

The Large Primality Challenge

The paper highlights $f_{46}(n) = 2^{2^n} + 93$ as beating Fermat's function: values are prime for $n = 1, \ldots, 6$. The corresponding theorem must certify primality of $2^{64} + 93 \approx 1.8 \times 10^{19}$. Similarly, Table 3 has a row of the same weight.

A norm_num proof would be a kernel-checked trial division with about $2^{31}$ steps, costing about an hour of build time. Instead, Lucas certificates are used: to certify $p$ prime, exhibit a witness $a$ with:

• $a^{p-1} \equiv 1 \pmod p$
• $a^{(p-1)/q} \not\equiv 1 \pmod p$ for each prime $q \mid p-1$

Mathlib supplies lucas_primality and the reduce_mod_char tactic. The only project-level glue is a lemma converting an explicit factorization of $p-1$ into lucas_primality's quantification:

theorem lucasCert (p a : N) (l : List N)
  (h1 : ∀ q ∈ l, Nat.Prime q)
  (hprod : p - 1 = l.prod)
  (h1 : (a : ZMod p) ^ (p - 1) = 1)
  (h2 : ∀ q ∈ l, (a : ZMod p) ^ ((p - 1) / q) ≠ 1) :
  Nat.Prime p

Sixteen certificates chain recursively down to primes small enough for norm_num's trial division, culminating in:

theorem prime_18446744073709551709 : Nat.Prime 18446744073709551709 := ...

Correspondence Table

Conclusion

This formalization demonstrates a complete, rigorous verification of a substantial mathematical paper's content. Key achievements include:

1. Full coverage: Every mathematical statement from the paper is formalized, with open questions deliberately left as unproved Prop statements.
2. Faithful reproduction: Proofs follow the paper's structure, including the subtle base-1 exception in Lemma 1.10.
3. Kernel-verified computation: All experimental results are checked by the Lean kernel, with the largest primality proofs using efficient Lucas certificates rather than naive trial division.
4. Principled extension: The extended class of Remark 3.4 is implemented and proved to genuinely extend the original class.
5. Dependency transparency: Every conditional theorem takes its hypotheses explicitly, making the logical structure of dependencies visible in each statement.