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

> This paper presents a complete Lean 4 formalization of "The Set of Primes is Supernatural," proving all 89 experimental table rows and all theorems except the central conjecture, which remains deliberately open.

- **Source:** [arXiv](https://arxiv.org/abs/2608.08643)
- **Published:** 2026-08-29
- **Permalink:** https://picx.dev/p/tt4SuE
- **Whiteboard:** https://picx.dev/p/tt4SuE/image

## Summary

# 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.

```lean
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:

```lean
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

```lean
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:

```lean
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:

```lean
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:

```lean
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:

```lean
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)$$

```lean
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:

```lean
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:

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

## Correspondence Table

| [3] | SPCL.lean | Status |
|-----|-----------|--------|
| Def. 1.1 (elevation structure) | `ElevationStructure` | formalized |
| — (morphism) | `ElevationHom` | formalized |
| — ("we obtain a category") | `ElevationHom.id`, `.comp`, laws, `Category ElevCat` instance | proved |
| Ex. 1.2, $\mathbb{I}$ | `instance : ElevationStructure N+` | formalized |
| Ex. 1.2, $\mathcal{F}$, $E_a$ | `instance : ElevationStructure (N+ → N+)`, `Eval` | formalized |
| Def. 1.3 ($A_+, A_\times, A_\wedge$) | `OpLetter`, `OpLetter.apply` | formalized |
| Def. 1.4 ($\Sigma$, $\mathcal{F}_{\text{Natural}}$) | `Word`, `Word.apply`, `Fs`, `FNatural` | formalized |
| — (inductive counterpart) | `IsNatural`; equivalence | proved |
| — ($\mathcal{F}_{\text{Natural}}$ elevation structure) | `FNatural_eq`, `instance : ElevationStructure {f // IsNatural f}` | formalized |
| Ex. 1.5 (a) $\mathcal{F}_s$ | `Fs_subset_FNatural` | proved |
| Ex. 1.5 (b) polynomials | `FPolynomial`, `FPolynomial_subset_words`, `FPolynomial_subset_FNatural` | proved |
| Ex. 1.5 (c) Fermat's word | `fermatFn_mem_word` | proved |
| Ex. 1.5 (d) four samples | `example_1_5_selfPow`, `_sevenPow`, `_big`, `_tower` | proved |
| Prop. 1.6 | `isNatural_constOrStrictMono` | proved |
| Def. 1.7 (length) | `natLength`, `natLength_spec` | proved |
| Lemmas 1.8, 1.9, 1.10 | `lemma_1_8`, `lemma_1_9`, `lemma_1_10` | proved |
| Remark 1.11 | `remark_1_11_*` (four statements) | proved |
| Conjecture 2.1 | `Conjecture_2_1` | stated (open) |
| §2.2 (supernatural sets) | `IsNaturalSet`, `IsSupernatural`, `conjecture_2_1_iff_supernatural`, `IsNaturalSet.infinite` | proved |
| Prop. 2.2(i) | `prop_2_2_i` | proved |
| Prop. 2.2(ii) | `prop_2_2_ii` | proved |
| Prop. 2.2(iii) | `fermatFn_five_eq`, `fermatFn_five_not_prime` | proved |
| Prop. 2.2(iv) | the 89 table theorems | proved |
| — | `IsNatural.comp` | proved (auxiliary for 3.1) |
| Prop. 3.1 | `proposition_3_1`; printed form `proposition_3_1_values` | proved (conditional) |
| Cor. 3.2 | `corollary_3_2` | proved (conditional) |
| Prop. 3.3 | `exists_all_prime_of_not_conjecture` | proved |
| Remark 3.4 (extended class) | `IsNaturalKnuthFactorialSub`, `IsNatural.toKnuthFactorialSub`, `Conjecture_KnuthFactorialSub` | stated (extension), embedding proved |
| §4, Table 1 | `table1_row1` – `table1_row10` | proved |
| §4, Table 2 (k = 1,...,59) | `table2_row1` – `table2_row59` | proved |
| §4, Table 3 (c = 2501,...,2539) | `table3_row2501` – `table3_row2539` | proved |
| — (primality certificates) | `Pratt.lucasCert`, sixteen `Pratt.prime_*` theorems | proved |
| §4, question (i) | `Question_i` | stated (open) |
| §4, question (ii) | not a determinate proposition as printed | not encoded |

## 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.

---

_Markdown view of https://picx.dev/p/tt4SuE, served by PicX — AI-generated visual whiteboard summaries of research papers._