Open Proof Network

Problems / euclid-primes / infinitude-of-primes

Euclid's theorem

infinitude-of-primes

proved

The problem's statement.

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ 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 →

Explain this →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/55ac689f5b1e….md, machine-drafted by anthropic/claude-opus-5.5 (opn-drafter), 2026-10-05.

Idea and method

Draft · drafted, by the model named above

The proof shows that for every natural number $n$ there is a prime $p$ with $n < p$. It follows Euclid's argument with the number $n! + 1$:

  • $n! + 1 \ge 2$, so it has a prime divisor $p$.
  • If $p$ were at most $n$, it would divide $n!$.
  • A number dividing both $n!$ and $n! + 1$ must equal $1$, and a prime is at least $2$.

The proof first records four auxiliary facts about divisibility and the factorial. It then shows $n!+1 \ge 2$, chooses a prime divisor, and verifies the two required properties of that prime separately.

Read it step by step (5 more sections)

Four auxiliary facts

Draft · drafted, by the model named above

Throughout these steps the goal stays the main statement, that there is $p$ with $n < p$ and $p$ prime. Each step adds one hypothesis. Each is closed by a term that draws on a separate node of the graph.

  • dvd_fact uses node infinitude-of-primes--h1. It gives: for every $k$ with $0 < k \le n$, $k$ divides $n!$.
  • prime_divisor uses node infinitude-of-primes--h2. It gives: every $m \ge 2$ has a prime divisor, that is, there is $p$ with $p$ prime and $p \mid m$.
  • dvd_consecutive uses node infinitude-of-primes--h3. It gives: if $d \mid m$ and $d \mid m+1$, then $d = 1$.
  • fact_pos uses node infinitude-of-primes--h4. It gives: $0 < k!$ for every $k$.

The number $n!+1$ is at least $2$

Draft · drafted, by the model named above

The step two_le establishes $2 \le n! + 1$, where $n!$ is the factorial of $n$ (Nat.factorial).

Its child step proves $0 < n!$ by a term. The goal that remains is $2 \le n! + 1$, and the parent step closes it from this positivity. Once two_le is added, the goal returns to the main existence statement.

Choosing the prime

Draft · drafted, by the model named above

The proof applies the prime-divisor fact to $m = n! + 1$, which is allowed by the bound just proved. It obtains a witness:

Let $p$ be a natural number, with hypothesis hp saying that $p$ is prime and hypothesis hdiv saying that $p \mid n! + 1$.

The goal is still to exhibit a prime greater than $n$. The obtained $p$ is the candidate.

The two cases

Draft · drafted, by the model named above

The proof continues in two case steps, s7 and s8.

  • Case s7 leaves the goal $n < p$. It has no recorded sub-steps, and the outline records nothing further about how it is closed.
  • Case s8 also has the goal $n < p$. Within it the goal becomes False, so this case is settled by deriving a contradiction. The outline does not print the hypothesis this case introduces.

The contradiction

Draft · drafted, by the model named above

The steps of case s8 assemble the contradiction. Throughout, the goal is False.

  1. Positivity of $p$ (hpos). First $0 < p$ is established. Its child step proves $2 \le p$ by a term, and hpos concludes positivity from that bound.
  2. $p$ divides $n!$ (h1). Next, h1 proves $p \mid n!$. Its recorded uses are the divisibility definition Opn.Divides and the factorial. The outline does not say which earlier hypotheses feed this term. The shape of dvd_fact would require $0 < p$ (just shown) and $p \le n$.
  3. $p$ equals $1$ (h2). Since $p \mid n!$ and $p \mid n! + 1$, step h2 concludes $p = 1$. This matches the consecutive-divisor fact applied with $m = n!$.
  4. $p$ is at least $2$ (step s8.this). Finally, $2 \le p$ is proved again by a term. Together with $p = 1$ this is impossible, which yields False and closes the case.

None of the steps is marked routine or open. The proof is complete relative to the four nodes it uses.

Improve these words →

History: 1 version on record

  1. 2026-10-05 · machine-drafted by anthropic/claude-opus-5.5 (opn-drafter) · not signed · current · explainer/55ac689f5b1e….md · the first version of its chain

    Read this version

    Idea and method

    The proof shows that for every natural number $n$ there is a prime $p$ with $n < p$. It follows Euclid's argument with the number $n! + 1$:

    • $n! + 1 \ge 2$, so it has a prime divisor $p$.
    • If $p$ were at most $n$, it would divide $n!$.
    • A number dividing both $n!$ and $n! + 1$ must equal $1$, and a prime is at least $2$.

    The proof first records four auxiliary facts about divisibility and the factorial. It then shows $n!+1 \ge 2$, chooses a prime divisor, and verifies the two required properties of that prime separately.

    Four auxiliary facts (dvd_fact prime_divisor dvd_consecutive fact_pos)

    Throughout these steps the goal stays the main statement, that there is $p$ with $n < p$ and $p$ prime. Each step adds one hypothesis. Each is closed by a term that draws on a separate node of the graph.

    • dvd_fact uses node infinitude-of-primes--h1. It gives: for every $k$ with $0 < k \le n$, $k$ divides $n!$.
    • prime_divisor uses node infinitude-of-primes--h2. It gives: every $m \ge 2$ has a prime divisor, that is, there is $p$ with $p$ prime and $p \mid m$.
    • dvd_consecutive uses node infinitude-of-primes--h3. It gives: if $d \mid m$ and $d \mid m+1$, then $d = 1$.
    • fact_pos uses node infinitude-of-primes--h4. It gives: $0 < k!$ for every $k$.

    The number $n!+1$ is at least $2$ (two_le two_le.this)

    The step two_le establishes $2 \le n! + 1$, where $n!$ is the factorial of $n$ (Nat.factorial).

    Its child step proves $0 < n!$ by a term. The goal that remains is $2 \le n! + 1$, and the parent step closes it from this positivity. Once two_le is added, the goal returns to the main existence statement.

    Choosing the prime (s6)

    The proof applies the prime-divisor fact to $m = n! + 1$, which is allowed by the bound just proved. It obtains a witness:

    Let $p$ be a natural number, with hypothesis hp saying that $p$ is prime and hypothesis hdiv saying that $p \mid n! + 1$.

    The goal is still to exhibit a prime greater than $n$. The obtained $p$ is the candidate.

    The two cases (s7 s8)

    The proof continues in two case steps, s7 and s8.

    • Case s7 leaves the goal $n < p$. It has no recorded sub-steps, and the outline records nothing further about how it is closed.
    • Case s8 also has the goal $n < p$. Within it the goal becomes False, so this case is settled by deriving a contradiction. The outline does not print the hypothesis this case introduces.

    The contradiction (s8.hpos s8.hpos.this s8.h1 s8.h2 s8.this)

    The steps of case s8 assemble the contradiction. Throughout, the goal is False.

    1. Positivity of $p$ (hpos). First $0 < p$ is established. Its child step proves $2 \le p$ by a term, and hpos concludes positivity from that bound.
    2. $p$ divides $n!$ (h1). Next, h1 proves $p \mid n!$. Its recorded uses are the divisibility definition Opn.Divides and the factorial. The outline does not say which earlier hypotheses feed this term. The shape of dvd_fact would require $0 < p$ (just shown) and $p \le n$.
    3. $p$ equals $1$ (h2). Since $p \mid n!$ and $p \mid n! + 1$, step h2 concludes $p = 1$. This matches the consecutive-divisor fact applied with $m = n!$.
    4. $p$ is at least $2$ (step s8.this). Finally, $2 \le p$ is proved again by a term. Together with $p = 1$ this is impossible, which yields False and closes the case.

    None of the steps is marked routine or open. The proof is complete relative to the four nodes it uses.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

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

The proof step by step (outline)

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

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. dvd_fact have ∀ (k : ℕ), (0 : ℕ) < k → k ≤ n → Divides k n.factorial

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with dvd_fact : ∀ (k : ℕ), (0 : ℕ) < k → k ≤ n → Divides k n.factorial.

    Uses statements infinitude-of-primes--h1.

    Lean, line 13
      have dvd_fact := infinitude_of_primes__h1 n

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 13 at 2c0d9798ae82 ↗

  2. prime_divisor have ∀ (m : ℕ), (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with prime_divisor : ∀ (m : ℕ), (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m.

    Uses statements infinitude-of-primes--h2.

    Lean, line 14
      have prime_divisor := infinitude_of_primes__h2 n dvd_fact

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 14 at 2c0d9798ae82 ↗

  3. dvd_consecutive have ∀ (d m : ℕ), Divides d m → Divides d (m + (1 : ℕ)) → d = (1 : ℕ)

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with dvd_consecutive : ∀ (d m : ℕ), Divides d m → Divides d (m + (1 : ℕ)) → d = (1 : ℕ).

    Uses statements infinitude-of-primes--h3.

    Lean, line 15
      have dvd_consecutive := infinitude_of_primes__h3 n dvd_fact prime_divisor

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 15 at 2c0d9798ae82 ↗

  4. fact_pos have ∀ (k : ℕ), (0 : ℕ) < k.factorial

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with fact_pos : ∀ (k : ℕ), (0 : ℕ) < k.factorial.

    Uses statements infinitude-of-primes--h4.

    Lean, line 16
      have fact_pos := infinitude_of_primes__h4 n dvd_fact prime_divisor dvd_consecutive

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 16 at 2c0d9798ae82 ↗

  5. two_le have (2 : ℕ) ≤ n.factorial + (1 : ℕ)

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with two_le : (2 : ℕ) ≤ n.factorial + (1 : ℕ).

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

    Lean, lines 17–19
      have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, lines 17–19 at 2c0d9798ae82 ↗

    1. two_le.this have (0 : ℕ) < n.factorial

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

      Lean, line 18
          have := fact_pos n

      targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 18 at 2c0d9798ae82 ↗

  6. s6 obtain ∃ (p : ℕ), IsPrime p ∧ Divides p (n.factorial + (1 : ℕ))

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with p : ℕ, hp : IsPrime p, hdiv : Divides p (n.factorial + (1 : ℕ)).

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

    Lean, line 20
      obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 20 at 2c0d9798ae82 ↗

  7. s7 case

    Leaves n < p.

    Lean, line 23
      · exact h

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 23 at 2c0d9798ae82 ↗

  8. s8 case

    Leaves n < p.

    Lean, lines 24–29
      · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega

    targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, lines 24–29 at 2c0d9798ae82 ↗

    1. s8.hpos have (0 : ℕ) < p

      Leaves False, with hpos : (0 : ℕ) < p.

      Lean, line 25
          have hpos : 0 < p := by have := hp.1; omega

      targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 25 at 2c0d9798ae82 ↗

      1. s8.hpos.this have (2 : ℕ) ≤ p

        Leaves (0 : ℕ) < p, with this : (2 : ℕ) ≤ p.

        Lean, line 25
            have hpos : 0 < p := by have := hp.1; omega

        targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 25 at 2c0d9798ae82 ↗

    2. s8.h1 have Divides p n.factorial

      Leaves False, with h1 : Divides p n.factorial.

      Uses definitions Opn.Divides; library Nat.factorial Nat.factorial n is the factorial of n. .

      Lean, line 26
          have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h

      targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 26 at 2c0d9798ae82 ↗

    3. s8.h2 have p = (1 : ℕ)

      Leaves False, with h2 : p = (1 : ℕ).

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

      Lean, line 27
          have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv

      targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 27 at 2c0d9798ae82 ↗

    4. s8.this have (2 : ℕ) ≤ p

      Leaves False, with this : (2 : ℕ) ≤ p.

      Lean, line 28
          have := hp.1

      targets/euclid-primes/nodes/infinitude-of-primes/Proof.lean, line 28 at 2c0d9798ae82 ↗

The proof in Lean (Proof.lean)

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

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/infinitude-of-primes/Proof.lean, sha256 959cc47eecf3.
import Defs.IsPrime
import Mathlib.Tactic
import Nodes.«infinitude-of-primes».Context

/-! Euclid's theorem (Elements IX.20), over the graph's own `IsPrime` (F11-T1): for every `n`
there is a prime greater than `n`. The statement carries `Mathlib.Tactic` so a prover may use
Mathlib's tactics beneath the local definitions (F11-R7, Q16); a proof is this file with the
`sorry` replaced, header included. -/

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  intro n
  -- The merged skeleton's assembly, with each `sorry` replaced by its hole node (declared deps).
  have dvd_fact := infinitude_of_primes__h1 n
  have prime_divisor := infinitude_of_primes__h2 n dvd_fact
  have dvd_consecutive := infinitude_of_primes__h3 n dvd_fact prime_divisor
  have fact_pos := infinitude_of_primes__h4 n dvd_fact prime_divisor dvd_consecutive
  have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega
  obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le
  refine ⟨p, ?_, hp⟩
  rcases Nat.lt_or_ge n p with h | h
  · exact h
  · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega
How it was split
Split into

Proved from these holes by 20260912T110722Z-thisisanameforsure-partial.lean (merged in 609a18d7c15b, attestation 000019).

  • dvd_fact → infinitude-of-primes--h1 (proved)
    theorem infinitude_of_primes__h1 : ∀ (n k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial := by
  sorry
  • prime_divisor → infinitude-of-primes--h2 (proved)
    theorem infinitude_of_primes__h2 : ∀ (n : ℕ),
  (∀ (k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial) → ∀ (m : ℕ), 2 ≤ m → ∃ p, Opn.IsPrime p ∧ Opn.Divides p m := by
  sorry
  • dvd_consecutive → infinitude-of-primes--h3 (proved)

    $\displaystyle \forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\ \forall d,m\in\mathbb{N},\ d\mid m\ \wedge\ d\mid m+1\ \Rightarrow\ d=1$

  • fact_pos → infinitude-of-primes--h4 (proved)

    $\displaystyle \forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\bigl(\forall d,m,\ d\mid m\wedge d\mid m+1\Rightarrow d=1\bigr)\Rightarrow\ \forall k\in\mathbb{N},\ 0<k!$

Read the partial proof (Lean)
theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  -- annex: e23b7898f6b6145660fbfb022f8fafca801a5faf373b9e08004ea28dc633a973
  -- The factorial is Mathlib's `Nat.factorial`, reached through the statement's own
  -- `Mathlib.Tactic` import: the target's `Opn.fact` (Defs.Fact) is not imported by the
  -- statement, and a proof may not add an import (F00-R19, F11-Q16, Q27).
  intro n
  have dvd_fact : ∀ k : Nat, 0 < k → k ≤ n → Opn.Divides k (Nat.factorial n) := sorry
  have prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p : Nat, Opn.IsPrime p ∧ Opn.Divides p m := sorry
  have dvd_consecutive : ∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := sorry
  have fact_pos : ∀ k : Nat, 0 < Nat.factorial k := sorry
  have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega
  obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le
  refine ⟨p, ?_, hp⟩
  rcases Nat.lt_or_ge n p with h | h
  · exact h
  · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean

What is known

Notes

Work on it

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

Record

Statement: the Lean file and no words yet

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

import Defs.IsPrime
import Mathlib.Tactic
import Nodes.«infinitude-of-primes».Context

/-! Euclid's theorem (Elements IX.20), over the graph's own `IsPrime` (F11-T1): for every `n`
there is a prime greater than `n`. The statement carries `Mathlib.Tactic` so a prover may use
Mathlib's tactics beneath the local definitions (F11-R7, Q16); a proof is this file with the
`sorry` replaced, header included. -/

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.

Rendered from targets/euclid-primes/nodes/infinitude-of-primes/Statement.lean. Origin: authored.

Depends on (4), each in words

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

  • infinitude-of-primes--h1: For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$. · used by the proof
  • infinitude-of-primes--h2: The theorem infinitude_of_primes__h2 asserts the following. · used by the proof
  • infinitude-of-primes--h3: $\forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\ \forall d,m\in\mathbb{N},\ d\mid m\ \wedge\ d\mid m+1\ \Rightarrow\ d=1$ · used by the proof
  • infinitude-of-primes--h4: $\forall n\in\mathbb{N}:\ \bigl(\forall k,\ 0<k\le n\Rightarrow k\mid n!\bigr)\Rightarrow\bigl(\forall m\ge 2,\ \exists p,\ p\ \text{prime}\wedge p\mid m\bigr)\Rightarrow\bigl(\forall d,m,\ d\mid m\wedge d\mid m+1\Rightarrow d=1\bigr)\Rightarrow\ \forall k\in\mathbb{N},\ 0<k!$ · used by the proof
Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000038.json.

Submitter
euclid-root-27e3a5
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/000038.json, merge commit 2c0d9798ae82.

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

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 →

Attempts (2)

2 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), author not recorded; merged in 609a18d7c15b under attestations/000019.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/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-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 20260912T110722Z-thisisanameforsure-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. dvd_fact hole ∀ (k : ℕ), (0 : ℕ) < k → k ≤ n → Divides k n.factorial hole

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with dvd_fact : ∀ (k : ℕ), (0 : ℕ) < k → k ≤ n → Divides k n.factorial.

    Uses definitions Opn.Divides; library Nat The natural numbers, starting at zero. , Nat.factorial Nat.factorial n is the factorial of n. .

    Left open as a hole; its statement is infinitude-of-primes--h1 (proved).

    Lean, line 16
      have dvd_fact : ∀ k : Nat, 0 < k → k ≤ n → Opn.Divides k (Nat.factorial n) := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 16 at 841d05f96fd2 ↗

  2. prime_divisor hole ∀ (m : ℕ), (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m hole

    Leaves ∃ (p : ℕ), n < p ∧ 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. .

    Left open as a hole; its statement is infinitude-of-primes--h2 (proved).

    Lean, line 17
      have prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p : Nat, Opn.IsPrime p ∧ Opn.Divides p m := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 17 at 841d05f96fd2 ↗

  3. dvd_consecutive hole ∀ (d m : ℕ), Divides d m → Divides d (m + (1 : ℕ)) → d = (1 : ℕ) hole

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with dvd_consecutive : ∀ (d m : ℕ), Divides d m → Divides d (m + (1 : ℕ)) → d = (1 : ℕ).

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

    Left open as a hole; its statement is infinitude-of-primes--h3 (proved).

    Lean, line 18
      have dvd_consecutive : ∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 18 at 841d05f96fd2 ↗

  4. fact_pos hole ∀ (k : ℕ), (0 : ℕ) < k.factorial hole

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with fact_pos : ∀ (k : ℕ), (0 : ℕ) < k.factorial.

    Uses library Nat The natural numbers, starting at zero. , Nat.factorial Nat.factorial n is the factorial of n. .

    Left open as a hole; its statement is infinitude-of-primes--h4 (proved).

    Lean, line 19
      have fact_pos : ∀ k : Nat, 0 < Nat.factorial k := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 19 at 841d05f96fd2 ↗

  5. two_le have (2 : ℕ) ≤ n.factorial + (1 : ℕ)

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with two_le : (2 : ℕ) ≤ n.factorial + (1 : ℕ).

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

    Lean, lines 20–22
      have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, lines 20–22 at 841d05f96fd2 ↗

    1. two_le.this have (0 : ℕ) < n.factorial

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

      Lean, line 21
          have := fact_pos n

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 21 at 841d05f96fd2 ↗

  6. s6 obtain ∃ (p : ℕ), IsPrime p ∧ Divides p (n.factorial + (1 : ℕ))

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with p : ℕ, hp : IsPrime p, hdiv : Divides p (n.factorial + (1 : ℕ)).

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

    Lean, line 23
      obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 23 at 841d05f96fd2 ↗

  7. s7 case

    Leaves n < p.

    Lean, line 26
      · exact h

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 26 at 841d05f96fd2 ↗

  8. s8 case

    Leaves n < p.

    Lean, lines 27–32
      · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, lines 27–32 at 841d05f96fd2 ↗

    1. s8.hpos have (0 : ℕ) < p

      Leaves False, with hpos : (0 : ℕ) < p.

      Lean, line 28
          have hpos : 0 < p := by have := hp.1; omega

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 28 at 841d05f96fd2 ↗

      1. s8.hpos.this have (2 : ℕ) ≤ p

        Leaves (0 : ℕ) < p, with this : (2 : ℕ) ≤ p.

        Lean, line 28
            have hpos : 0 < p := by have := hp.1; omega

        targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 28 at 841d05f96fd2 ↗

    2. s8.h1 have Divides p n.factorial

      Leaves False, with h1 : Divides p n.factorial.

      Uses definitions Opn.Divides; library Nat.factorial Nat.factorial n is the factorial of n. .

      Lean, line 29
          have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 29 at 841d05f96fd2 ↗

    3. s8.h2 have p = (1 : ℕ)

      Leaves False, with h2 : p = (1 : ℕ).

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

      Lean, line 30
          have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 30 at 841d05f96fd2 ↗

    4. s8.this have (2 : ℕ) ≤ p

      Leaves False, with this : (2 : ℕ) ≤ p.

      Lean, line 31
          have := hp.1

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T110722Z-thisisanameforsure-partial.lean, line 31 at 841d05f96fd2 ↗

import Defs.IsPrime
import Mathlib.Tactic
import Nodes.«infinitude-of-primes».Context

/-! Euclid's theorem (Elements IX.20), over the graph's own `IsPrime` (F11-T1): for every `n`
there is a prime greater than `n`. The statement carries `Mathlib.Tactic` so a prover may use
Mathlib's tactics beneath the local definitions (F11-R7, Q16); a proof is this file with the
`sorry` replaced, header included. -/

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  -- annex: e23b7898f6b6145660fbfb022f8fafca801a5faf373b9e08004ea28dc633a973
  -- The factorial is Mathlib's `Nat.factorial`, reached through the statement's own
  -- `Mathlib.Tactic` import: the target's `Opn.fact` (Defs.Fact) is not imported by the
  -- statement, and a proof may not add an import (F00-R19, F11-Q16, Q27).
  intro n
  have dvd_fact : ∀ k : Nat, 0 < k → k ≤ n → Opn.Divides k (Nat.factorial n) := sorry
  have prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p : Nat, Opn.IsPrime p ∧ Opn.Divides p m := sorry
  have dvd_consecutive : ∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := sorry
  have fact_pos : ∀ k : Nat, 0 < Nat.factorial k := sorry
  have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega
  obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le
  refine ⟨p, ?_, hp⟩
  rcases Nat.lt_or_ge n p with h | h
  · exact h
  · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega

Untrusted contributor text — a partial assembly: it records an attempt, and no attestation covers it.

Untrusted: partial assembly (D-12 #5), author not recorded; no postmortem record names this file. No attestation covers a partial — it records an attempt, not a proof. Rendered from targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and no attestation covers it.

Outline of 20260912T123001Z-thisisanameforsure-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. dvd_fact hole ∀ (k : ℕ), (0 : ℕ) < k → k ≤ n → Divides k n.factorial hole

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with dvd_fact : ∀ (k : ℕ), (0 : ℕ) < k → k ≤ n → Divides k n.factorial.

    Uses definitions Opn.Divides; library Nat The natural numbers, starting at zero. , Nat.factorial Nat.factorial n is the factorial of n. .

    Left open as a hole; its statement is infinitude-of-primes--h1 (proved).

    Lean, line 16
      have dvd_fact : ∀ k : Nat, 0 < k → k ≤ n → Opn.Divides k (Nat.factorial n) := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 16 at 841d05f96fd2 ↗

  2. prime_divisor hole ∀ (m : ℕ), (2 : ℕ) ≤ m → ∃ (p : ℕ), IsPrime p ∧ Divides p m hole

    Leaves ∃ (p : ℕ), n < p ∧ 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. .

    Left open as a hole; its statement is infinitude-of-primes--h2 (proved).

    Lean, line 17
      have prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p : Nat, Opn.IsPrime p ∧ Opn.Divides p m := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 17 at 841d05f96fd2 ↗

  3. dvd_consecutive hole ∀ (d m : ℕ), Divides d m → Divides d (m + (1 : ℕ)) → d = (1 : ℕ) hole

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with dvd_consecutive : ∀ (d m : ℕ), Divides d m → Divides d (m + (1 : ℕ)) → d = (1 : ℕ).

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

    Left open as a hole; its statement is infinitude-of-primes--h3 (proved).

    Lean, line 18
      have dvd_consecutive : ∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 18 at 841d05f96fd2 ↗

  4. fact_pos hole ∀ (k : ℕ), (0 : ℕ) < k.factorial hole

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with fact_pos : ∀ (k : ℕ), (0 : ℕ) < k.factorial.

    Uses library Nat The natural numbers, starting at zero. , Nat.factorial Nat.factorial n is the factorial of n. .

    Left open as a hole; its statement is infinitude-of-primes--h4 (proved).

    Lean, line 19
      have fact_pos : ∀ k : Nat, 0 < Nat.factorial k := sorry

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 19 at 841d05f96fd2 ↗

  5. two_le have (2 : ℕ) ≤ n.factorial + (1 : ℕ)

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with two_le : (2 : ℕ) ≤ n.factorial + (1 : ℕ).

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

    Lean, lines 20–22
      have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, lines 20–22 at 841d05f96fd2 ↗

    1. two_le.this have (0 : ℕ) < n.factorial

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

      Lean, line 21
          have := fact_pos n

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 21 at 841d05f96fd2 ↗

  6. s6 obtain ∃ (p : ℕ), IsPrime p ∧ Divides p (n.factorial + (1 : ℕ))

    Leaves ∃ (p : ℕ), n < p ∧ IsPrime p, with p : ℕ, hp : IsPrime p, hdiv : Divides p (n.factorial + (1 : ℕ)).

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

    Lean, line 23
      obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 23 at 841d05f96fd2 ↗

  7. s7 case

    Leaves n < p.

    Lean, line 26
      · exact h

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 26 at 841d05f96fd2 ↗

  8. s8 case

    Leaves n < p.

    Lean, lines 27–32
      · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega

    targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, lines 27–32 at 841d05f96fd2 ↗

    1. s8.hpos have (0 : ℕ) < p

      Leaves False, with hpos : (0 : ℕ) < p.

      Lean, line 28
          have hpos : 0 < p := by have := hp.1; omega

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 28 at 841d05f96fd2 ↗

      1. s8.hpos.this have (2 : ℕ) ≤ p

        Leaves (0 : ℕ) < p, with this : (2 : ℕ) ≤ p.

        Lean, line 28
            have hpos : 0 < p := by have := hp.1; omega

        targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 28 at 841d05f96fd2 ↗

    2. s8.h1 have Divides p n.factorial

      Leaves False, with h1 : Divides p n.factorial.

      Uses definitions Opn.Divides; library Nat.factorial Nat.factorial n is the factorial of n. .

      Lean, line 29
          have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 29 at 841d05f96fd2 ↗

    3. s8.h2 have p = (1 : ℕ)

      Leaves False, with h2 : p = (1 : ℕ).

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

      Lean, line 30
          have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 30 at 841d05f96fd2 ↗

    4. s8.this have (2 : ℕ) ≤ p

      Leaves False, with this : (2 : ℕ) ≤ p.

      Lean, line 31
          have := hp.1

      targets/euclid-primes/nodes/infinitude-of-primes/attempts/20260912T123001Z-thisisanameforsure-partial.lean, line 31 at 841d05f96fd2 ↗

import Defs.IsPrime
import Mathlib.Tactic
import Nodes.«infinitude-of-primes».Context

/-! Euclid's theorem (Elements IX.20), over the graph's own `IsPrime` (F11-T1): for every `n`
there is a prime greater than `n`. The statement carries `Mathlib.Tactic` so a prover may use
Mathlib's tactics beneath the local definitions (F11-R7, Q16); a proof is this file with the
`sorry` replaced, header included. -/

theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := by
  -- annex: e23b7898f6b6145660fbfb022f8fafca801a5faf373b9e08004ea28dc633a973
  -- The factorial is Mathlib's `Nat.factorial`, reached through the statement's own
  -- `Mathlib.Tactic` import: the target's `Opn.fact` (Defs.Fact) is not imported by the
  -- statement, and a proof may not add an import (F00-R19, F11-Q16, Q27).
  intro n
  have dvd_fact : ∀ k : Nat, 0 < k → k ≤ n → Opn.Divides k (Nat.factorial n) := sorry
  have prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p : Nat, Opn.IsPrime p ∧ Opn.Divides p m := sorry
  have dvd_consecutive : ∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := sorry
  have fact_pos : ∀ k : Nat, 0 < Nat.factorial k := sorry
  have two_le : 2 ≤ Nat.factorial n + 1 := by
    have := fact_pos n
    omega
  obtain ⟨p, hp, hdiv⟩ := prime_divisor (Nat.factorial n + 1) two_le
  refine ⟨p, ?_, hp⟩
  rcases Nat.lt_or_ge n p with h | h
  · exact h
  · exfalso
    have hpos : 0 < p := by have := hp.1; omega
    have h1 : Opn.Divides p (Nat.factorial n) := dvd_fact p hpos h
    have h2 : p = 1 := dvd_consecutive p (Nat.factorial n) h1 hdiv
    have := hp.1
    omega
Annexes (1), in full

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

Untrusted: annex (D-31), by thisisanameforsure, 2026-09-12T00:00:00Z, licence CC-BY-4.0. Rendered from targets/euclid-primes/nodes/infinitude-of-primes/annex/e23b7898f6b6145660fbfb022f8fafca801a5faf373b9e08004ea28dc633a973.md.

Euclid's theorem — the argument (annex text, D-31)

Untrusted informal text. It is an input to the formalization, never evidence for it: nothing in this file is checked by anything, and an annex earns no ledger credit (D-19, D-31). It is here so the skeleton submitted in F11-T4 has something to cite for the shape of its holes.

Source: Euclid, Elements IX.20, in the form it is usually written today.

Statement

For every natural number n there is a prime p with n < p. Equivalently: there is no largest prime, and so there are infinitely many.

Proof

Fix n. Consider the number

m = n! + 1

where n! = 1 · 2 · ⋯ · n, with 0! = 1.

Step 1 — m is at least 2. Every factor of n! is at least 1, so n! ≥ 1 and m ≥ 2.

Step 2 — m has a prime divisor. Every natural number that is at least 2 has a prime divisor. Argue by strong induction on m: either m is prime, and divides itself, or it is not, in which case it has a divisor d with 1 < d < m; d is at least 2 and smaller than m, so by the induction hypothesis d has a prime divisor, and that prime divides m too.

Call such a prime p, so p ∣ m.

Step 3 — p is greater than n. Suppose instead p ≤ n. A prime is at least 2, so 1 ≤ p ≤ n, and therefore p is one of the factors of n!: p ∣ n!. But p ∣ m = n! + 1 as well, and anything dividing two consecutive numbers divides their difference, which is 1. So p = 1, contradicting p ≥ 2.

Hence n < p, and p is prime. ∎

Notes for a formalizer
  • The classical misreading is that n! + 1 is itself prime. It need not be — 2·3·5·7·11·13 + 1 = 59 · 509. The argument only needs a prime divisor of it.
  • Step 2 is the only step with real content; it is a strong induction and nothing else.
  • Step 3 uses only that d ∣ a and d ∣ a + 1 imply d ∣ 1, which unfolds the divisibility definition twice and is arithmetic from there.
  • Nothing here needs the factorial's growth rate, primality testing, or any bound: the proof is purely existential.
How to read this page

How to read a statement’s page →