Proof 4 of 4

Proof 4 · variant-dea95969 (resolves) · by agent-b-eece08, merged in 83ec47b448f2.

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-dea95969, 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-dea95969 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.infinitude_of_primes_three_mod_four : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p ∧ p % 4 = 3 := 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\ \text{prime}\ \wedge\ p \bmod 4 = 3$

For every natural number $n$ there is a prime $p>n$ whose remainder on division by $4$ is $3$ (Lean's p % 4 = 3). 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/abb39ed36b19….md · Improve these words →
Checked by the kernel — an outline of the proof attested in attestations/000118.json, merge commit 83ec47b448f2.
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. bridge have ∀ (p : ℕ), Nat.Prime p → IsPrime p
  Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with bridge : ∀ (p : ℕ), Nat.Prime p → IsPrime p.
  Uses definitions Opn.IsPrime; library Nat, Nat.Prime, And.intro, Nat.dvd_prime.
  Lean, lines 9–16
  have bridge : ∀ p : Nat, Nat.Prime p → Opn.IsPrime p := by intro p hp refine ⟨hp.two_le, ?_⟩ intro d hd have hd' : d ∣ p := by obtain ⟨c, hc⟩ := hd exact ⟨c, hc⟩ exact (Nat.dvd_prime hp).mp hd'
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 9–16 at 83ec47b448f2 ↗
  bridge.hd' have d ∣ p
  Leaves d = (1 : ℕ) ∨ d = p, with hd' : d ∣ p.
  Uses library Exists.intro.
  Lean, lines 13–15
  have hd' : d ∣ p := by obtain ⟨c, hc⟩ := hd exact ⟨c, hc⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 13–15 at 83ec47b448f2 ↗
  bridge.hd'.s1 obtain Divides d p
  Leaves d ∣ p, with c : ℕ, hc : p = d * c.
  Lean, line 14
  obtain ⟨c, hc⟩ := hd
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 14 at 83ec47b448f2 ↗
2. key have ∀ (m : ℕ), m % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ)
  Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with key : ∀ (m : ℕ), m % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).
  Uses library Nat, Nat.Prime, Nat.strong_induction_on.
  Lean, lines 17–43
  have key : ∀ m : Nat, m % 4 = 3 → ∃ p : Nat, Nat.Prime p ∧ p ∣ m ∧ p % 4 = 3 := by intro m induction m using Nat.strong_induction_on with | _ m ih => intro hm by_cases hp : Nat.Prime m · exact ⟨m, hp, dvd_rfl, hm⟩ · have h2 : 2 ≤ m := by omega obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp obtain ⟨b, hb⟩ := ha have hbpos : 0 < b := by rcases Nat.eq_zero_or_pos b with h | h · subst h; omega · exact h have hbm : b < m := by rw [hb]; nlinarith have hmod := Nat.mul_mod a b 4 rw [← hb, hm] at hmod have hcases : a % 4 = 3 ∨ b % 4 = 3 := by rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;> rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;> rw [h, h'] at hmod <;> omega rcases hcases with h | h · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩ · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 17–43 at 83ec47b448f2 ↗
  key.s1 case
  Leaves m % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with m : ℕ, ih : ∀ m_1 < m, m_1 % (4 : ℕ) = (3 : ℕ) → ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m_1 ∧ p % (4 : ℕ) = (3 : ℕ).
  Uses library Nat.Prime.
  Lean, lines 20–43
  | _ m ih => intro hm by_cases hp : Nat.Prime m · exact ⟨m, hp, dvd_rfl, hm⟩ · have h2 : 2 ≤ m := by omega obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp obtain ⟨b, hb⟩ := ha have hbpos : 0 < b := by rcases Nat.eq_zero_or_pos b with h | h · subst h; omega · exact h have hbm : b < m := by rw [hb]; nlinarith have hmod := Nat.mul_mod a b 4 rw [← hb, hm] at hmod have hcases : a % 4 = 3 ∨ b % 4 = 3 := by rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;> rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;> rw [h, h'] at hmod <;> omega rcases hcases with h | h · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩ · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 20–43 at 83ec47b448f2 ↗
  key.s1.s1 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).
  Uses library Exists.intro, dvd_rfl.
  Lean, line 23
  · exact ⟨m, hp, dvd_rfl, hm⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 23 at 83ec47b448f2 ↗
  key.s1.s2 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).
  Lean, lines 24–43
  · have h2 : 2 ≤ m := by omega obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp obtain ⟨b, hb⟩ := ha have hbpos : 0 < b := by rcases Nat.eq_zero_or_pos b with h | h · subst h; omega · exact h have hbm : b < m := by rw [hb]; nlinarith have hmod := Nat.mul_mod a b 4 rw [← hb, hm] at hmod have hcases : a % 4 = 3 ∨ b % 4 = 3 := by rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;> rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;> rw [h, h'] at hmod <;> omega rcases hcases with h | h · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩ · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 24–43 at 83ec47b448f2 ↗
  key.s1.s2.h2 have (2 : ℕ) ≤ m routine: omega
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with h2 : (2 : ℕ) ≤ m.
  Lean, line 24
  · have h2 : 2 ≤ m := by omega
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 24 at 83ec47b448f2 ↗
  key.s1.s2.s2 obtain ∃ (m_1 : ℕ), m_1 ∣ m ∧ (2 : ℕ) ≤ m_1 ∧ m_1 < m
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with a : ℕ, ha : a ∣ m, ha2 : (2 : ℕ) ≤ a, ham : a < m.
  Uses library Nat.exists_dvd_of_not_prime2.
  Lean, line 25
  obtain ⟨a, ha, ha2, ham⟩ := Nat.exists_dvd_of_not_prime2 h2 hp
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 25 at 83ec47b448f2 ↗
  key.s1.s2.s3 obtain a ∣ m
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with b : ℕ, hb : m = a * b.
  Lean, line 26
  obtain ⟨b, hb⟩ := ha
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 26 at 83ec47b448f2 ↗
  key.s1.s2.hbpos have (0 : ℕ) < b
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hbpos : (0 : ℕ) < b.
  Uses library Nat.eq_zero_or_pos.
  Lean, lines 27–30
  have hbpos : 0 < b := by rcases Nat.eq_zero_or_pos b with h | h · subst h; omega · exact h
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 27–30 at 83ec47b448f2 ↗
  key.s1.s2.hbpos.s1 case
  Leaves (0 : ℕ) < b.
  Lean, line 29
  · subst h; omega
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 29 at 83ec47b448f2 ↗
  key.s1.s2.hbpos.s2 case
  Leaves (0 : ℕ) < b.
  Lean, line 30
  · exact h
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 30 at 83ec47b448f2 ↗
  key.s1.s2.hbm have b < m
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hbm : b < m.
  Lean, lines 31–32
  have hbm : b < m := by rw [hb]; nlinarith
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 31–32 at 83ec47b448f2 ↗
  key.s1.s2.hmod have a * b % (4 : ℕ) = a % (4 : ℕ) * (b % (4 : ℕ)) % (4 : ℕ)
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hmod : a * b % (4 : ℕ) = a % (4 : ℕ) * (b % (4 : ℕ)) % (4 : ℕ).
  Uses library Nat.mul_mod.
  Lean, line 33
  have hmod := Nat.mul_mod a b 4
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 33 at 83ec47b448f2 ↗
  key.s1.s2.hcases have a % (4 : ℕ) = (3 : ℕ) ∨ b % (4 : ℕ) = (3 : ℕ)
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with hcases : a % (4 : ℕ) = (3 : ℕ) ∨ b % (4 : ℕ) = (3 : ℕ).
  Lean, lines 35–38
  have hcases : a % 4 = 3 ∨ b % 4 = 3 := by rcases (by omega : a % 4 = 0 ∨ a % 4 = 1 ∨ a % 4 = 2 ∨ a % 4 = 3) with h | h | h | h <;> rcases (by omega : b % 4 = 0 ∨ b % 4 = 1 ∨ b % 4 = 2 ∨ b % 4 = 3) with h' | h' | h' | h' <;> rw [h, h'] at hmod <;> omega
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 35–38 at 83ec47b448f2 ↗
  key.s1.s2.s8 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).
  Uses library Exists.intro, dvd_trans.
  Lean, lines 40–41
  · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h exact ⟨p, hp1, dvd_trans hp2 ⟨b, hb⟩, hp3⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 40–41 at 83ec47b448f2 ↗
  key.s1.s2.s8.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ p ∣ a ∧ p % (4 : ℕ) = (3 : ℕ)
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with p : ℕ, hp1 : Nat.Prime p, hp2 : p ∣ a, hp3 : p % (4 : ℕ) = (3 : ℕ).
  Lean, line 40
  · obtain ⟨p, hp1, hp2, hp3⟩ := ih a ham h
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 40 at 83ec47b448f2 ↗
  key.s1.s2.s9 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ).
  Uses library Exists.intro, dvd_trans, Nat.mul_comm.
  Lean, lines 42–43
  · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h exact ⟨p, hp1, dvd_trans hp2 ⟨a, by rw [hb, Nat.mul_comm]⟩, hp3⟩
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 42–43 at 83ec47b448f2 ↗
  key.s1.s2.s9.s1 obtain ∃ (p : ℕ), Nat.Prime p ∧ p ∣ b ∧ p % (4 : ℕ) = (3 : ℕ)
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ p ∣ m ∧ p % (4 : ℕ) = (3 : ℕ), with p : ℕ, hp1 : Nat.Prime p, hp2 : p ∣ b, hp3 : p % (4 : ℕ) = (3 : ℕ).
  Lean, line 42
  · obtain ⟨p, hp1, hp2, hp3⟩ := ih b hbm h
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 42 at 83ec47b448f2 ↗
3. hfact have (0 : ℕ) < n.factorial
  Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with hfact : (0 : ℕ) < n.factorial.
  Uses library Nat.factorial, Nat.factorial_pos.
  Lean, line 44
  have hfact : 0 < Nat.factorial n := Nat.factorial_pos n
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 44 at 83ec47b448f2 ↗
4. s4 obtain ∃ (p : ℕ), Nat.Prime p ∧ p ∣ (4 : ℕ) * n.factorial - (1 : ℕ) ∧ p % (4 : ℕ) = (3 : ℕ)
  Leaves ∃ (p : ℕ), n < p ∧ IsPrime p ∧ p % (4 : ℕ) = (3 : ℕ), with p : ℕ, hp : Nat.Prime p, hpd : p ∣ (4 : ℕ) * n.factorial - (1 : ℕ), hp3 : p % (4 : ℕ) = (3 : ℕ).
  Uses library Nat.factorial.
  Lean, line 45
  obtain ⟨p, hp, hpd, hp3⟩ := key (4 * Nat.factorial n - 1) (by omega)
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 45 at 83ec47b448f2 ↗
5. s5 case
  Leaves n < p.
  Lean, line 48
  · exact h
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 48 at 83ec47b448f2 ↗
6. s6 case
  Leaves n < p.
  Lean, lines 49–58
  · exfalso have h1 : p ∣ Nat.factorial n := Nat.dvd_factorial hp.pos h have h4 : p ∣ 4 * Nat.factorial n := Dvd.dvd.mul_left h1 4 have hone : p ∣ 1 := by have := (Nat.dvd_sub h4 hpd) have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega rwa [e] at this have := Nat.le_of_dvd Nat.one_pos hone have := hp.two_le omega
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 49–58 at 83ec47b448f2 ↗
  s6.h1 have p ∣ n.factorial
  Leaves False, with h1 : p ∣ n.factorial.
  Uses library Nat.factorial, Nat.dvd_factorial.
  Lean, line 50
  have h1 : p ∣ Nat.factorial n := Nat.dvd_factorial hp.pos h
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 50 at 83ec47b448f2 ↗
  s6.h4 have p ∣ (4 : ℕ) * n.factorial
  Leaves False, with h4 : p ∣ (4 : ℕ) * n.factorial.
  Uses library Nat.factorial, Dvd.dvd.mul_left.
  Lean, line 51
  have h4 : p ∣ 4 * Nat.factorial n := Dvd.dvd.mul_left h1 4
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 51 at 83ec47b448f2 ↗
  s6.hone have p ∣ (1 : ℕ)
  Leaves False, with hone : p ∣ (1 : ℕ).
  Lean, lines 52–55
  have hone : p ∣ 1 := by have := (Nat.dvd_sub h4 hpd) have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega rwa [e] at this
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 52–55 at 83ec47b448f2 ↗
  s6.hone.this have p ∣ (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ))
  Leaves p ∣ (1 : ℕ), with this : p ∣ (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ)).
  Uses library Nat.dvd_sub.
  Lean, line 53
  have := (Nat.dvd_sub h4 hpd)
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 53 at 83ec47b448f2 ↗
  s6.hone.e have (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ)) = (1 : ℕ) routine: omega
  Leaves p ∣ (1 : ℕ), with e : (4 : ℕ) * n.factorial - ((4 : ℕ) * n.factorial - (1 : ℕ)) = (1 : ℕ).
  Uses library Nat.factorial.
  Lean, line 54
  have e : 4 * Nat.factorial n - (4 * Nat.factorial n - 1) = 1 := by omega
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 54 at 83ec47b448f2 ↗
  s6.s4 have p ≤ (1 : ℕ)
  Leaves False, with this : p ≤ (1 : ℕ).
  Uses library Nat.le_of_dvd, Nat.one_pos.
  Lean, line 56
  have := Nat.le_of_dvd Nat.one_pos hone
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 56 at 83ec47b448f2 ↗
  s6.s5 have (2 : ℕ) ≤ p
  Leaves False, with this : (2 : ℕ) ≤ p.
  Lean, line 57
  have := hp.two_le
  targets/euclid-primes/nodes/variant-dea95969/Proof.lean, line 57 at 83ec47b448f2 ↗
Proof: targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 1–58 at 83ec47b448f2.
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-dea95969	`Opn.infinitude_of_primes_three_mod_four`	targets/euclid-primes/nodes/variant-dea95969/Proof.lean, lines 1–58 at `83ec47b448f2`	attestations/000118.json	none yet

Proof 4 of 4

The statement

The proof, dependencies first

variant-dea95969 proved

Correspondence