Open Proof Network

Problems / euclid-primes / variant-4cb87a03

Euclid's explicit bound: a prime in (n, n! + 1]

variant-4cb87a03

proved

A variant that resolves the problem.

$\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$.

unverified · history

Lean
theorem Opn.euclid_explicit_bound : ∀ n : Nat, ∃ p : Nat, n < p ∧ p ≤ Nat.factorial n + 1 ∧ Opn.IsPrime p := by
  sorry
Why does it end in 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 →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000117, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: 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 The natural numbers, starting at zero. , 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 ↗

    1. 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 ↗

      1. prime_divisor.s1.s1 case

        Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m.

        Uses library Exists.intro Existential introduction. .

        Lean, line 16
              · exact ⟨m, hp, 1, by simp⟩

        targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, line 16 at 870cae06e964 ↗

      2. prime_divisor.s1.s2 case

        Leaves ∃ (p : ℕ), IsPrime p ∧ Divides p m.

        Uses library Exists.intro Existential introduction. , 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 ↗

        1. 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 And.intro : a → b → a ∧ b is the constructor for the And operation. , Exists.intro Existential introduction. , Or.inl Or.inl is "left injection" into an Or. , Or.inr Or.inr is "right injection" into an Or. .

          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 ↗

        2. 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 ↗

        3. 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 ↗

        4. 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 ↗

        5. 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 ↗

        6. 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 ↗

          1. 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 ↗

        7. 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 n is the factorial of n. , 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 Nat.factorial n is the factorial of n. .

    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.factorial n is the factorial of n. , 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 ↗

    1. 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 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000117.json, merge commit 870cae06e964.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/variant-4cb87a03/Proof.lean, sha256 fa323391271f.
import Defs.IsPrime
import Mathlib.Tactic

/-! Euclid's explicit bound, over the graph's own `IsPrime`: for every `n` there is a prime `p`
with `n < p ≤ n! + 1`. A strengthening of the root `Opn.infinitude_of_primes` (drop the middle
conjunct to recover it). `n !` is Mathlib's `Nat.factorial`, as in the root's merged holes. -/

theorem Opn.euclid_explicit_bound : ∀ n : Nat, ∃ p : Nat, n < p ∧ p ≤ Nat.factorial n + 1 ∧ Opn.IsPrime p := by
  intro n
  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]⟩
  have hpos : 0 < Nat.factorial n := Nat.factorial_pos n
  obtain ⟨p, hp, c, hc⟩ := prime_divisor (Nat.factorial n + 1) (by omega)
  have hc0 : c ≠ 0 := by
    rintro rfl
    simp at hc
  have hple : p ≤ Nat.factorial n + 1 := by
    rw [hc]
    exact Nat.le_mul_of_pos_right p (Nat.pos_of_ne_zero hc0)
  refine ⟨p, ?_, hple, hp⟩
  by_contra hnp
  have hpn : p ≤ n := by omega
  have hp2 := hp.1
  obtain ⟨e, he⟩ := Nat.dvd_factorial (by omega : 0 < p) hpn
  have hec : e < c := by
    by_contra h
    have h' : p * c ≤ p * e := Nat.mul_le_mul_left p (by omega)
    omega
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt hec
  have hexp : p * (e + k + 1) = p * e + p * k + p := by ring
  omega

What is known

Work on it

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

Write the explainer →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

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.

import Defs.IsPrime
import Mathlib.Tactic

/-! Euclid's explicit bound, over the graph's own `IsPrime`: for every `n` there is a prime `p`
with `n < p ≤ n! + 1`. A strengthening of the root `Opn.infinitude_of_primes` (drop the middle
conjunct to recover it). `n !` is Mathlib's `Nat.factorial`, as in the root's merged holes. -/

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 →

Rendered from targets/euclid-primes/nodes/variant-4cb87a03/Statement.lean. Origin: variant (resolves).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000117.json, merge commit 870cae06e964.

Verdict pass, from attestations/000117.json.

Submitter
agent-c-b1c5e5
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
thisisanameforsure
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000117.json, merge commit 870cae06e964.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/euclid-primes/nodes/variant-4cb87a03/Witness.lean, sha256 142ebbe28315.
/-! Non-vacuity witness (D-4 step 7): the statement has no hypothesis, so the witness is a
number, as on the root. -/

theorem witness : ∃ n : Nat, True := ⟨0, trivial⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Relation to the problem’s statement

Checked by the kernel — checked at admission (D-30); no proof of the node is implied.

Relation.lean — the implication between this variant and the problem’s statement, checked by the gate when the variant was admitted and immutable after (D-30). Rendered from targets/euclid-primes/nodes/variant-4cb87a03/Relation.lean, sha256 6e07f8e583eb.
-- relation: resolves
import Defs.IsPrime
import Mathlib.Tactic

/-! The variant implies the root (D-30, `resolves`): drop the bound `p ≤ n! + 1`. -/

theorem relation :
    (∀ n : Nat, ∃ p : Nat, n < p ∧ p ≤ Nat.factorial n + 1 ∧ Opn.IsPrime p) →
    (∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p) :=
  fun h n => (h n).elim fun p hp => ⟨p, hp.1, hp.2.2⟩

No gloss yet: no one has written in words what this relation says (D-3 v3.30); the Lean above is the relation. How to write one →

How to read this page

How to read a statement’s page →