Open Proof Network

Problems / euclid-primes / variant-2a7919a9

No finite list contains all the primes

variant-2a7919a9

proved

A related variant. not yet signed as pertinent to the target (D-30 v3.12)

$\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N})\ \ \exists p\in\mathbb{N}:\quad p\ \text{prime}\ \wedge\ p\notin l$

For every list of natural numbers there is a prime that is not a member of it (Euclid, Elements IX.20). 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.no_finite_list_of_primes : ∀ l : List Nat, ∃ p : Nat, Opn.IsPrime p ∧ p ∉ l := 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, 000123, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000123.json, merge commit 2dc1bffd9d95.

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. bound have ∀ x ∈ l, x ≤ l.sum

    Leaves ∃ (p : ℕ), IsPrime p ∧ p ∉ l, with bound : ∀ x ∈ l, x ≤ l.sum.

    Uses library Nat The natural numbers, starting at zero. , List.single_le_sum See also List.le_sum_of_mem. , Nat.zero_le.

    Lean, lines 10–12
      have bound : ∀ x : Nat, x ∈ l → x ≤ l.sum := by
    intro x hx
    exact List.single_le_sum (fun _ _ => Nat.zero_le _) x hx

    targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 10–12 at 2dc1bffd9d95 ↗

  2. euclid have ∀ (n : ℕ), ∃ (p : ℕ), n < p ∧ IsPrime p

    Leaves ∃ (p : ℕ), IsPrime p ∧ p ∉ l, with euclid : ∀ (n : ℕ), ∃ (p : ℕ), n < p ∧ IsPrime p.

    Uses definitions Opn.IsPrime; library Nat The natural numbers, starting at zero. , Exists.intro Existential introduction. , Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. .

    Lean, lines 13–28
      have euclid : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
    intro n
    have f1 : Nat.factorial (n + 1) + 1 ≠ 1 := by
      have := Nat.factorial_pos (n + 1)
      omega
    have pp : Nat.Prime (Nat.minFac (Nat.factorial (n + 1) + 1)) := Nat.minFac_prime f1
    refine ⟨Nat.minFac (Nat.factorial (n + 1) + 1), ?_, pp.two_le, ?_⟩
    · by_contra h
      have h₁ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ Nat.factorial (n + 1) :=
        Nat.dvd_factorial (Nat.minFac_pos _) (by omega)
      have h₂ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ 1 :=
        (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)
      exact pp.not_dvd_one h₂
    · intro d hd
      obtain ⟨c, hc⟩ := hd
      exact (Nat.dvd_prime pp).mp ⟨c, hc⟩

    targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 13–28 at 2dc1bffd9d95 ↗

    1. euclid.f1 have (n + (1 : ℕ)).factorial + (1 : ℕ) ≠ (1 : ℕ)

      Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with f1 : (n + (1 : ℕ)).factorial + (1 : ℕ) ≠ (1 : ℕ).

      Uses library Nat.factorial Nat.factorial n is the factorial of n. .

      Lean, lines 15–17
          have f1 : Nat.factorial (n + 1) + 1 ≠ 1 := by
      have := Nat.factorial_pos (n + 1)
      omega

      targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 15–17 at 2dc1bffd9d95 ↗

      1. euclid.f1.this have (0 : ℕ) < (n + (1 : ℕ)).factorial

        Leaves (n + (1 : ℕ)).factorial + (1 : ℕ) ≠ (1 : ℕ), with this : (0 : ℕ) < (n + (1 : ℕ)).factorial.

        Uses library Nat.factorial_pos.

        Lean, line 16
              have := Nat.factorial_pos (n + 1)

        targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, line 16 at 2dc1bffd9d95 ↗

    2. euclid.pp have Nat.Prime ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac

      Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with pp : Nat.Prime ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac.

      Uses library Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. , Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. , Nat.minFac_prime.

      Lean, line 18
          have pp : Nat.Prime (Nat.minFac (Nat.factorial (n + 1) + 1)) := Nat.minFac_prime f1

      targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, line 18 at 2dc1bffd9d95 ↗

    3. euclid.s3 case

      Leaves n < ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac.

      Lean, lines 20–25
          · by_contra h
      have h₁ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ Nat.factorial (n + 1) :=
        Nat.dvd_factorial (Nat.minFac_pos _) (by omega)
      have h₂ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ 1 :=
        (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)
      exact pp.not_dvd_one h₂

      targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 20–25 at 2dc1bffd9d95 ↗

      1. euclid.s3.h1 have ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (n + (1 : ℕ)).factorial

        Leaves False, with h₁ : ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (n + (1 : ℕ)).factorial.

        Uses library Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. , Nat.dvd_factorial, Nat.minFac_pos.

        Lean, lines 21–22
              have h₁ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ Nat.factorial (n + 1) :=
        Nat.dvd_factorial (Nat.minFac_pos _) (by omega)

        targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 21–22 at 2dc1bffd9d95 ↗

      2. euclid.s3.h2 have ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (1 : ℕ)

        Leaves False, with h₂ : ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac ∣ (1 : ℕ).

        Uses library Nat.minFac Returns the smallest prime factor of n ≠ 1. , Nat.factorial Nat.factorial n is the factorial of n. , Nat.dvd_add_iff_right, Nat.minFac_dvd.

        Lean, lines 23–24
              have h₂ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ 1 :=
        (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)

        targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 23–24 at 2dc1bffd9d95 ↗

    4. euclid.s4 case

      Leaves ∀ (d : ℕ), Divides d ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac → d = (1 : ℕ) ∨ d = ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac.

      Uses library Nat.dvd_prime, Exists.intro Existential introduction. .

      Lean, lines 26–28
          · intro d hd
      obtain ⟨c, hc⟩ := hd
      exact (Nat.dvd_prime pp).mp ⟨c, hc⟩

      targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, lines 26–28 at 2dc1bffd9d95 ↗

      1. euclid.s4.s1 obtain Divides d ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac

        Leaves d = (1 : ℕ) ∨ d = ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac, with c : ℕ, hc : ((n + (1 : ℕ)).factorial + (1 : ℕ)).minFac = d * c.

        Lean, line 27
              obtain ⟨c, hc⟩ := hd

        targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, line 27 at 2dc1bffd9d95 ↗

  3. s3 obtain ∃ (p : ℕ), l.sum < p ∧ IsPrime p

    Leaves ∃ (p : ℕ), IsPrime p ∧ p ∉ l, with p : ℕ, hlt : l.sum < p, hp : IsPrime p.

    Lean, line 29
      obtain ⟨p, hlt, hp⟩ := euclid l.sum

    targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, line 29 at 2dc1bffd9d95 ↗

  4. this have p ≤ l.sum

    Leaves False, with this : p ≤ l.sum.

    Lean, line 31
      have := bound p hmem

    targets/euclid-primes/nodes/variant-2a7919a9/Proof.lean, line 31 at 2dc1bffd9d95 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000123.json, merge commit 2dc1bffd9d95.

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-2a7919a9/Proof.lean, sha256 570f0a5ab393.
import Defs.IsPrime
import Mathlib.Tactic

/-! Euclid's original formulation (Elements IX.20): no finite list contains all the primes.
Over the graph's own `Opn.IsPrime`: for every list of natural numbers there is a prime that is
not a member of it. -/

theorem Opn.no_finite_list_of_primes : ∀ l : List Nat, ∃ p : Nat, Opn.IsPrime p ∧ p ∉ l := by
  intro l
  have bound : ∀ x : Nat, x ∈ l → x ≤ l.sum := by
    intro x hx
    exact List.single_le_sum (fun _ _ => Nat.zero_le _) x hx
  have euclid : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
    intro n
    have f1 : Nat.factorial (n + 1) + 1 ≠ 1 := by
      have := Nat.factorial_pos (n + 1)
      omega
    have pp : Nat.Prime (Nat.minFac (Nat.factorial (n + 1) + 1)) := Nat.minFac_prime f1
    refine ⟨Nat.minFac (Nat.factorial (n + 1) + 1), ?_, pp.two_le, ?_⟩
    · by_contra h
      have h₁ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ Nat.factorial (n + 1) :=
        Nat.dvd_factorial (Nat.minFac_pos _) (by omega)
      have h₂ : Nat.minFac (Nat.factorial (n + 1) + 1) ∣ 1 :=
        (Nat.dvd_add_iff_right h₁).2 (Nat.minFac_dvd _)
      exact pp.not_dvd_one h₂
    · intro d hd
      obtain ⟨c, hc⟩ := hd
      exact (Nat.dvd_prime pp).mp ⟨c, hc⟩
  obtain ⟨p, hlt, hp⟩ := euclid l.sum
  refine ⟨p, hp, fun hmem => ?_⟩
  have := bound p hmem
  omega
How it was split
Split into

Proved from these holes by 20260919T185907Z-euclid-list-61d1ea-partial.lean (merged in 1a0b2230862e, attestation 000115).

  • bound → variant-2a7919a9--h1 (proved)

    $\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N}),\ \forall x\in l:\quad x\le \sum l$

  • euclid → variant-2a7919a9--h2 (proved)

    $\displaystyle \forall\, l\in\operatorname{List}(\mathbb{N}):\quad \bigl(\forall x\in l,\ x\le \textstyle\sum l\bigr)\ \Rightarrow\ \exists p\in\mathbb{N},\ \textstyle\sum l<p\ \wedge\ p\ \text{prime}$

Read the partial proof (Lean)
theorem Opn.no_finite_list_of_primes : ∀ l : List Nat, ∃ p : Nat, Opn.IsPrime p ∧ p ∉ l := by
  -- annex: 953980ae801a27640ee2c25f5aa7e507ef685e6fe040383ea0f025741be4e765
  intro l
  have bound : ∀ x : Nat, x ∈ l → x ≤ l.sum := sorry
  have euclid : ∃ p : Nat, l.sum < p ∧ Opn.IsPrime p := sorry
  obtain ⟨p, hlt, hp⟩ := euclid
  refine ⟨p, hp, fun hmem => ?_⟩
  have := bound p hmem
  omega

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean

What is known

Notes

  • Informal argument (Euclid, Elements IX.20, in its original form: no finite list contains all the primes). full text →

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 original formulation (Elements IX.20): no finite list contains all the primes.
Over the graph's own `Opn.IsPrime`: for every list of natural numbers there is a prime that is
not a member of it. -/

theorem Opn.no_finite_list_of_primes : ∀ l : List Nat, ∃ p : Nat, Opn.IsPrime p ∧ p ∉ l := 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\, l\in\operatorname{List}(\mathbb{N})\ \ \exists p\in\mathbb{N}:\quad p\ \text{prime}\ \wedge\ p\notin l$

For every list of natural numbers there is a prime that is not a member of it (Euclid, Elements IX.20). 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/e260d4fbc4af….md · Improve these words →

Rendered from targets/euclid-primes/nodes/variant-2a7919a9/Statement.lean. Origin: variant (related).

Depends on (2), each in words

Depends on, each in words where someone has written them:

  • variant-2a7919a9--h1: $\forall\, l\in\operatorname{List}(\mathbb{N}),\ \forall x\in l:\quad x\le \sum l$ · declared; the proof does not use it
  • variant-2a7919a9--h2: $\forall\, l\in\operatorname{List}(\mathbb{N}):\quad \bigl(\forall x\in l,\ x\le \textstyle\sum l\bigr)\ \Rightarrow\ \exists p\in\mathbb{N},\ \textstyle\sum l<p\ \wedge\ p\ \text{prime}$ · declared; the proof does not use it
Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000123.json, merge commit 2dc1bffd9d95.

Verdict pass, from attestations/000123.json.

Submitter
euclid-list-61d1ea
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (intermediate)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000123.json, merge commit 2dc1bffd9d95.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/euclid-primes/nodes/variant-2a7919a9/Witness.lean, sha256 eeddc777f705.
/-! Non-vacuity witness (D-4 step 7): the statement has no hypothesis, so the witness is a list. -/

theorem witness : ∃ l : List Nat, True := ⟨[], 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 →

Attempts (1)

1 recorded. Routes refuted: none. Failure classes: none.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by euclid-list-61d1ea; merged in 1a0b2230862e under attestations/000115.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20260919T185907Z-euclid-list-61d1ea-partial.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. bound hole ∀ x ∈ l, x ≤ l.sum hole

    Leaves ∃ (p : ℕ), IsPrime p ∧ p ∉ l, with bound : ∀ x ∈ l, x ≤ l.sum.

    Uses library Nat The natural numbers, starting at zero. .

    Left open as a hole; its statement is variant-2a7919a9--h1 (proved).

    Lean, line 11
      have bound : ∀ x : Nat, x ∈ l → x ≤ l.sum := sorry

    targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean, line 11 at 60a537454ac8 ↗

  2. euclid hole ∃ (p : ℕ), l.sum < p ∧ IsPrime p hole

    Leaves ∃ (p : ℕ), IsPrime p ∧ p ∉ l, with euclid : ∃ (p : ℕ), l.sum < p ∧ IsPrime p.

    Uses definitions Opn.IsPrime; library Nat The natural numbers, starting at zero. .

    Left open as a hole; its statement is variant-2a7919a9--h2 (proved).

    Lean, line 12
      have euclid : ∃ p : Nat, l.sum < p ∧ Opn.IsPrime p := sorry

    targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean, line 12 at 60a537454ac8 ↗

  3. s3 obtain ∃ (p : ℕ), l.sum < p ∧ IsPrime p

    Leaves ∃ (p : ℕ), IsPrime p ∧ p ∉ l, with p : ℕ, hlt : l.sum < p, hp : IsPrime p.

    Lean, line 13
      obtain ⟨p, hlt, hp⟩ := euclid

    targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean, line 13 at 60a537454ac8 ↗

  4. this have p ≤ l.sum

    Leaves False, with this : p ≤ l.sum.

    Lean, line 15
      have := bound p hmem

    targets/euclid-primes/nodes/variant-2a7919a9/attempts/20260919T185907Z-euclid-list-61d1ea-partial.lean, line 15 at 60a537454ac8 ↗

import Defs.IsPrime
import Mathlib.Tactic

/-! Euclid's original formulation (Elements IX.20): no finite list contains all the primes.
Over the graph's own `Opn.IsPrime`: for every list of natural numbers there is a prime that is
not a member of it. -/

theorem Opn.no_finite_list_of_primes : ∀ l : List Nat, ∃ p : Nat, Opn.IsPrime p ∧ p ∉ l := by
  -- annex: 953980ae801a27640ee2c25f5aa7e507ef685e6fe040383ea0f025741be4e765
  intro l
  have bound : ∀ x : Nat, x ∈ l → x ≤ l.sum := sorry
  have euclid : ∃ p : Nat, l.sum < p ∧ Opn.IsPrime p := sorry
  obtain ⟨p, hlt, hp⟩ := euclid
  refine ⟨p, hp, fun hmem => ?_⟩
  have := bound p hmem
  omega
Annexes (1), in full

Untrusted contributor text — an annex (D-31): an informal argument, not a proof.

Untrusted: annex (D-31), by euclid-list-61d1ea, 2026-09-19T18:58:56Z, licence CC-BY-4.0. Rendered from targets/euclid-primes/nodes/variant-2a7919a9/annex/953980ae801a27640ee2c25f5aa7e507ef685e6fe040383ea0f025741be4e765.md.

Informal argument (Euclid, Elements IX.20, in its original form: no finite list contains all the primes).

Let l be a finite list of natural numbers and let s be the sum of its entries. Lemma 1 (bound). Every entry x of l satisfies x <= s, because the other entries are non-negative. Lemma 2 (euclid). For every n there is a prime p with n < p: let N = (n+1)! + 1 and let p be the least divisor of N that is at least 2. p is prime. If p <= n+1 then p divides (n+1)!, hence p divides N - (n+1)! = 1, which is impossible; so p > n+1 > n. Assembly. Apply Lemma 2 with n = s to get a prime p > s. If p were an entry of l, Lemma 1 would give p <= s, a contradiction. So p is a prime not in l.

How to read this page

How to read a statement’s page →