Proof 3 of 4

Proof 3 · variant-4cb87a03 (resolves) · by agent-c-b1c5e5, merged in 870cae06e964.

The statement

Statement not audited — fidelity mechanical-only; QA pass incomplete; no signer yet.

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.

For every natural number n there is a prime greater than n.

Fidelity: statement unchecked. Rendered from targets/euclid-primes/nodes/infinitude-of-primes/Statement.lean. This proof proves variant-4cb87a03, a variant that resolves the problem (D-30).

The proof, dependencies first

1 statement on this proof. Each statement comes before the statements whose proofs use it. A step’s outline is folded; open it for its goal, what it uses and its Lean lines. How to read a proof page →

variant-4cb87a03 proved
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
```
theorem Opn.euclid_explicit_bound : ∀ n : Nat, ∃ p : Nat, n < p ∧ p ≤ Nat.factorial n + 1 ∧ Opn.IsPrime p := by
  sorry
```
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ p\le n!+1\ \wedge\ p\ \text{prime}$

For every natural number $n$ there is a prime $p$ with $n<p\le n!+1$, where $n!$ is Mathlib's Nat.factorial. Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.
Rendered from gloss/e629f13a0d5c….md · Improve these words →
Checked by the kernel — an outline of the proof attested in attestations/000117.json, merge commit 870cae06e964.
Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.
1. prime_divisor have ∀ (m : ℕ), (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m
  Leaves ∃ (p : ℕ), n < p ∧ p ≤ n.factorial + (1 : ℕ) ∧ IsPrime p, with prime_divisor : ∀ (m : ℕ), (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m.
  Uses definitions Opn.IsPrime, Opn.Divides; library Nat, Nat.strong_induction_on.
  Lean, lines 10–40
  have prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p, Opn.IsPrime p ∧ Opn.Divides p m := by intro m induction m using Nat.strong_induction_on with | _ m ih => intro hm by_cases hp : Opn.IsPrime m · exact ⟨m, hp, 1, by simp⟩ · have hex : ∃ d, Opn.Divides d m ∧ d ≠ 1 ∧ d ≠ m := by by_contra hcon apply hp refine ⟨hm, fun d hd => ?_⟩ by_contra h exact hcon ⟨d, hd, fun h1 => h (Or.inl h1), fun h2 => h (Or.inr h2)⟩ obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hex have hd0 : d ≠ 0 := by rintro rfl simp at hc omega have hc0 : c ≠ 0 := by rintro rfl simp at hc omega have hc1 : c ≠ 1 := by rintro rfl simp at hc exact hdm hc.symm have hdlt : d < m := by have h2 : d * 2 ≤ d * c := Nat.mul_le_mul_left d (by omega) omega obtain ⟨p, hp', q, hq⟩ := ih d hdlt (by omega) exact ⟨p, hp', q * c, by rw [hc, hq, Nat.mul_assoc]⟩
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 10–40 at 870cae06e964 ↗
  prime_divisor.s1 case
  Leaves (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m, with m : ℕ, ih : ∀ m_1 < m, (2 : ℕ) ≤ m_1 → ∃ (p : ℕ), IsPrime p ∧ Divides p m_1.
  Uses definitions Opn.IsPrime.
  Lean, lines 13–40
  | _ m ih => intro hm by_cases hp : Opn.IsPrime m · exact ⟨m, hp, 1, by simp⟩ · have hex : ∃ d, Opn.Divides d m ∧ d ≠ 1 ∧ d ≠ m := by by_contra hcon apply hp refine ⟨hm, fun d hd => ?_⟩ by_contra h exact hcon ⟨d, hd, fun h1 => h (Or.inl h1), fun h2 => h (Or.inr h2)⟩ obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hex have hd0 : d ≠ 0 := by rintro rfl simp at hc omega have hc0 : c ≠ 0 := by rintro rfl simp at hc omega have hc1 : c ≠ 1 := by rintro rfl simp at hc exact hdm hc.symm have hdlt : d < m := by have h2 : d * 2 ≤ d * c := Nat.mul_le_mul_left d (by omega) omega obtain ⟨p, hp', q, hq⟩ := ih d hdlt (by omega) exact ⟨p, hp', q * c, by rw [hc, hq, Nat.mul_assoc]⟩
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 13–40 at 870cae06e964 ↗
  prime_divisor.s1.s1 case
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m.
  Uses library Exists.intro.
  Lean, line 16
  · exact ⟨m, hp, 1, by simp⟩
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 16 at 870cae06e964 ↗
  prime_divisor.s1.s2 case
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m.
  Uses library Exists.intro, Nat.mul_assoc.
  Lean, lines 17–40
  · have hex : ∃ d, Opn.Divides d m ∧ d ≠ 1 ∧ d ≠ m := by by_contra hcon apply hp refine ⟨hm, fun d hd => ?_⟩ by_contra h exact hcon ⟨d, hd, fun h1 => h (Or.inl h1), fun h2 => h (Or.inr h2)⟩ obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hex have hd0 : d ≠ 0 := by rintro rfl simp at hc omega have hc0 : c ≠ 0 := by rintro rfl simp at hc omega have hc1 : c ≠ 1 := by rintro rfl simp at hc exact hdm hc.symm have hdlt : d < m := by have h2 : d * 2 ≤ d * c := Nat.mul_le_mul_left d (by omega) omega obtain ⟨p, hp', q, hq⟩ := ih d hdlt (by omega) exact ⟨p, hp', q * c, by rw [hc, hq, Nat.mul_assoc]⟩
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 17–40 at 870cae06e964 ↗
  prime_divisor.s1.s2.hex have ∃ (d : ℕ), Divides d m ∧ d ≠ (1 : ℕ) ∧ d ≠ m
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with hex : ∃ (d : ℕ), Divides d m ∧ d ≠ (1 : ℕ) ∧ d ≠ m.
  Uses definitions Opn.Divides; library And.intro, Exists.intro, Or.inl, Or.inr.
  Lean, lines 17–22
  · have hex : ∃ d, Opn.Divides d m ∧ d ≠ 1 ∧ d ≠ m := by by_contra hcon apply hp refine ⟨hm, fun d hd => ?_⟩ by_contra h exact hcon ⟨d, hd, fun h1 => h (Or.inl h1), fun h2 => h (Or.inr h2)⟩
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 17–22 at 870cae06e964 ↗
  prime_divisor.s1.s2.s2 obtain ∃ (d : ℕ), Divides d m ∧ d ≠ (1 : ℕ) ∧ d ≠ m
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with d : ℕ, c : ℕ, hc : m = d * c, hd1 : d ≠ (1 : ℕ), hdm : d ≠ m.
  Lean, line 23
  obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hex
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 23 at 870cae06e964 ↗
  prime_divisor.s1.s2.hd0 have d ≠ (0 : ℕ)
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with hd0 : d ≠ (0 : ℕ).
  Lean, lines 24–27
  have hd0 : d ≠ 0 := by rintro rfl simp at hc omega
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 24–27 at 870cae06e964 ↗
  prime_divisor.s1.s2.hc0 have c ≠ (0 : ℕ)
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with hc0 : c ≠ (0 : ℕ).
  Lean, lines 28–31
  have hc0 : c ≠ 0 := by rintro rfl simp at hc omega
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 28–31 at 870cae06e964 ↗
  prime_divisor.s1.s2.hc1 have c ≠ (1 : ℕ)
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with hc1 : c ≠ (1 : ℕ).
  Lean, lines 32–35
  have hc1 : c ≠ 1 := by rintro rfl simp at hc exact hdm hc.symm
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 32–35 at 870cae06e964 ↗
  prime_divisor.s1.s2.hdlt have d < m
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with hdlt : d < m.
  Lean, lines 36–38
  have hdlt : d < m := by have h2 : d * 2 ≤ d * c := Nat.mul_le_mul_left d (by omega) omega
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 36–38 at 870cae06e964 ↗
  prime_divisor.s1.s2.hdlt.h2 have d * (2 : ℕ) ≤ d * c
  Leaves d < m, with h2 : d * (2 : ℕ) ≤ d * c.
  Uses library Nat.mul_le_mul_left.
  Lean, line 37
  have h2 : d * 2 ≤ d * c := Nat.mul_le_mul_left d (by omega)
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 37 at 870cae06e964 ↗
  prime_divisor.s1.s2.s7 obtain ∃ (p : ℕ), IsPrime p ∧ Divides p d
  Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m, with p : ℕ, hp' : IsPrime p, q : ℕ, hq : d = p * q.
  Lean, line 39
  obtain ⟨p, hp', q, hq⟩ := ih d hdlt (by omega)
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 39 at 870cae06e964 ↗
2. hpos have (0 : ℕ) < n.factorial
  Leaves ∃ (p : ℕ), n < p ∧ p ≤ n.factorial + (1 : ℕ) ∧ IsPrime p, with hpos : (0 : ℕ) < n.factorial.
  Uses library Nat.factorial, Nat.factorial_pos.
  Lean, line 41
  have hpos : 0 < Nat.factorial n := Nat.factorial_pos n
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 41 at 870cae06e964 ↗
3. s3 obtain ∃ (p : ℕ), IsPrime p ∧ Divides p (n.factorial + (1 : ℕ))
  Leaves ∃ (p : ℕ), n < p ∧ p ≤ n.factorial + (1 : ℕ) ∧ IsPrime p, with p : ℕ, hp : IsPrime p, c : ℕ, hc : n.factorial + (1 : ℕ) = p * c.
  Uses library Nat.factorial.
  Lean, line 42
  obtain ⟨p, hp, c, hc⟩ := prime_divisor (Nat.factorial n + 1) (by omega)
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 42 at 870cae06e964 ↗
4. hc0 have c ≠ (0 : ℕ)
  Leaves ∃ (p : ℕ), n < p ∧ p ≤ n.factorial + (1 : ℕ) ∧ IsPrime p, with hc0 : c ≠ (0 : ℕ).
  Lean, lines 43–45
  have hc0 : c ≠ 0 := by rintro rfl simp at hc
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 43–45 at 870cae06e964 ↗
5. hple have p ≤ n.factorial + (1 : ℕ)
  Leaves ∃ (p : ℕ), n < p ∧ p ≤ n.factorial + (1 : ℕ) ∧ IsPrime p, with hple : p ≤ n.factorial + (1 : ℕ).
  Uses library Nat.factorial, Nat.le_mul_of_pos_right, Nat.pos_of_ne_zero.
  Lean, lines 46–48
  have hple : p ≤ Nat.factorial n + 1 := by rw [hc] exact Nat.le_mul_of_pos_right p (Nat.pos_of_ne_zero hc0)
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 46–48 at 870cae06e964 ↗
6. hpn have p ≤ n routine: omega
  Leaves False, with hpn : p ≤ n.
  Lean, line 51
  have hpn : p ≤ n := by omega
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 51 at 870cae06e964 ↗
7. hp2 have (2 : ℕ) ≤ p
  Leaves False, with hp2 : (2 : ℕ) ≤ p.
  Lean, line 52
  have hp2 := hp.1
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 52 at 870cae06e964 ↗
8. s8 obtain p ∣ n.factorial
  Leaves False, with e : ℕ, he : n.factorial = p * e.
  Uses library Nat.dvd_factorial.
  Lean, line 53
  obtain ⟨e, he⟩ := Nat.dvd_factorial (by omega : 0 < p) hpn
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 53 at 870cae06e964 ↗
9. hec have e < c
  Leaves False, with hec : e < c.
  Lean, lines 54–57
  have hec : e < c := by by_contra h have h' : p * c ≤ p * e := Nat.mul_le_mul_left p (by omega) omega
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 54–57 at 870cae06e964 ↗
  hec.h' have p * c ≤ p * e
  Leaves False, with h' : p * c ≤ p * e.
  Uses library Nat.mul_le_mul_left.
  Lean, line 56
  have h' : p * c ≤ p * e := Nat.mul_le_mul_left p (by omega)
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 56 at 870cae06e964 ↗
10. s10 obtain ∃ (k : ℕ), c = e + k + (1 : ℕ)
  Leaves False, with k : ℕ, hc : n.factorial + (1 : ℕ) = p * (e + k + (1 : ℕ)), hc0 : e + k + (1 : ℕ) ≠ (0 : ℕ), hec : e < e + k + (1 : ℕ).
  Uses library Nat.exists_eq_add_of_lt.
  Lean, line 58
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hec
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 58 at 870cae06e964 ↗
11. hexp have p * (e + k + (1 : ℕ)) = p * e + p * k + p routine: ring
  Leaves False, with hexp : p * (e + k + (1 : ℕ)) = p * e + p * k + p.
  Lean, line 59
  have hexp : p * (e + k + 1) = p * e + p * k + p := by ring
  targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 59 at 870cae06e964 ↗
Proof: targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 1–60 at 870cae06e964.
No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Correspondence

Checked by the kernel — each row’s declaration, file, lines and attestation are the attested record; the explainer column says only whether unverified prose exists and who signed it.

Statement	Declaration	Proof file and lines	Attestation	Explainer
variant-4cb87a03	`Opn.euclid_explicit_bound`	targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, lines 1–60 at `870cae06e964`	attestations/000117.json	none yet

Proof 3 of 4

The statement

The proof, dependencies first

variant-4cb87a03 proved

Correspondence