Problems / euclid-primes / proof 1

Proof 1 of 4

Proof 1 · root · by euclid-root-27e3a5, merged in 2c0d9798ae82.

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

The proof, dependencies first

5 statements 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 →

1. infinitude-of-primes--h1 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 infinitude_of_primes__h1 : ∀ (n k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial := 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 f21-words-check, drafted with anthropic/claude-opus-5.5 via Claude Code, 2026-10-05; read against the Lean by thisisanameforsure (2026-10-06) (F20-R8; it changes no status or grade).

   Final · read against the Lean by thisisanameforsure (2026-10-06)

   For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$.

   Divisibility here is the problem's own definition Opn.Divides: $k$ divides $m$ when $m = k \cdot c$ for some natural number $c$.

   Rendered from gloss/df65addf582c….md · Improve these words →

   History: 2 versions on record

   1. 2026-10-05 · written by f21-words-check, drafted with anthropic/claude-opus-5.5 via Claude Code · signed by thisisanameforsure (2026-10-06) · gloss/df65addf582c….md · the first version of its chain

      Read this version

      For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$.

      Divisibility here is the problem's own definition Opn.Divides: $k$ divides $m$ when $m = k \cdot c$ for some natural number $c$.

   2. 2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/db3494256811….md · diff to its predecessor

      Read this version

      For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$.

      Divisibility here is the problem's own definition Opn.Divides: $k$ divides $m$ when $m = k \cdot c$ for some natural number $c$.

   Diff of db3494256811 against df65addf582c

   (the words are the same)

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

   Checked by the kernel — an outline of the proof attested in attestations/000034.json, merge commit a9f10904c037.

   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. s1 obtain k ∣ n.factorial

      Leaves Opn.Divides k n.factorial, with c : ℕ, hc : n.factorial = k * c.

      Uses library Nat.dvd_factorial.

      Lean, line 10

        obtain ⟨c, hc⟩ := Nat.dvd_factorial hk hkn

      targets/euclid-primes/nodes/infinitude-of-primes--h1/Proof.lean, line 10 at a9f10904c037 ↗

   Proof: targets/euclid-primes/nodes/infinitude-of-primes--h1/Proof.lean, lines 1–11 at a9f10904c037.

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

2. infinitude-of-primes--h2 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 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

   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; machine-drafted by anthropic/claude-opus-5.5 (opn-drafter), 2026-10-05; no one has read it against the Lean and signed it.

   Draft · drafted, by the model named above

   The theorem infinitude_of_primes__h2 asserts the following. For every natural number $n$, suppose every natural number $k$ with $0 < k$ and $k \le n$ divides $n!$, where "divides" is Opn.Divides. Under that hypothesis, for every natural number $m$ with $2 \le m$ there exists some $p$ such that $p$ is prime and $p$ divides $m$. Here "prime" is Opn.IsPrime and "divides" is again Opn.Divides.

   The hypothesis about $n$ does not mention $m$ or $p$, so the conclusion does not depend on $n$. The file does not write the type of $p$; it is whatever argument type Opn.IsPrime and Opn.Divides take. No gloss of either definition from Defs.IsPrime was provided, so their meanings are taken from their names only. The proof in the file is sorry.

   Rendered from gloss/000e299f1638….md · Improve these words →

   History: 2 versions on record

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

      Read this version

      The theorem infinitude_of_primes__h2 asserts the following. For every natural number $n$, suppose every natural number $k$ with $0 < k$ and $k \le n$ divides $n!$, where "divides" is Opn.Divides. Under that hypothesis, for every natural number $m$ with $2 \le m$ there exists some $p$ such that $p$ is prime and $p$ divides $m$. Here "prime" is Opn.IsPrime and "divides" is again Opn.Divides.

      The hypothesis about $n$ does not mention $m$ or $p$, so the conclusion does not depend on $n$. The file does not write the type of $p$; it is whatever argument type Opn.IsPrime and Opn.Divides take. No gloss of either definition from Defs.IsPrime was provided, so their meanings are taken from their names only. The proof in the file is sorry.

   2. 2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/e5c72899d9e2….md · diff to its predecessor

      Read this version

      The theorem infinitude_of_primes__h2 asserts the following. For every natural number $n$, suppose every natural number $k$ with $0 < k$ and $k \le n$ divides $n!$, where "divides" is Opn.Divides. Under that hypothesis, for every natural number $m$ with $2 \le m$ there exists some $p$ such that $p$ is prime and $p$ divides $m$. Here "prime" is Opn.IsPrime and "divides" is again Opn.Divides.

      The hypothesis about $n$ does not mention $m$ or $p$, so the conclusion does not depend on $n$. The file does not write the type of $p$; it is whatever argument type Opn.IsPrime and Opn.Divides take. No gloss of either definition from Defs.IsPrime was provided, so their meanings are taken from their names only. The proof in the file is sorry.

   Diff of e5c72899d9e2 against 000e299f1638

   (the words are the same)

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

   Checked by the kernel — an outline of the proof attested in attestations/000035.json, merge commit b134abca6e5d.

   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. s1 case

      Leaves (2 : ℕ) ≤ m → ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m, with m : ℕ, ih : ∀ m_1 < m, (2 : ℕ) ≤ m_1 → ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m_1.

      Uses definitions Opn.IsPrime.

      Lean, lines 12–25

        | _ m ih =>
          intro hm
          by_cases hp : Opn.IsPrime m
          · exact ⟨m, hp, 1, (Nat.mul_one m).symm⟩
          · have hnot : ¬ ∀ d : Nat, Opn.Divides d m → d = 1 ∨ d = m := fun h => hp ⟨hm, h⟩
            push_neg at hnot
            obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hnot
            have hd0 : d ≠ 0 := by
              intro h
              rw [h, Nat.zero_mul] at hc
              omega
            have hdle : d ≤ m := Nat.le_of_dvd (by omega) ⟨c, hc⟩
            obtain ⟨p, hpp, a, ha⟩ := ih d (by omega) (by omega)
            exact ⟨p, hpp, a * c, by rw [hc, ha, Nat.mul_assoc]⟩

      targets/euclid-primes/nodes/infinitude-of-primes--h2/Proof.lean, lines 12–25 at b134abca6e5d ↗

      1. s1.s1 case

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

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

         Lean, line 15

             · exact ⟨m, hp, 1, (Nat.mul_one m).symm⟩

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

      2. s1.s2 case

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

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

         Lean, lines 16–25

             · have hnot : ¬ ∀ d : Nat, Opn.Divides d m → d = 1 ∨ d = m := fun h => hp ⟨hm, h⟩
               push_neg at hnot
               obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hnot
               have hd0 : d ≠ 0 := by
                 intro h
                 rw [h, Nat.zero_mul] at hc
                 omega
               have hdle : d ≤ m := Nat.le_of_dvd (by omega) ⟨c, hc⟩
               obtain ⟨p, hpp, a, ha⟩ := ih d (by omega) (by omega)
               exact ⟨p, hpp, a * c, by rw [hc, ha, Nat.mul_assoc]⟩

         targets/euclid-primes/nodes/infinitude-of-primes--h2/Proof.lean, lines 16–25 at b134abca6e5d ↗

         1. s1.s2.hnot have ¬∀ (d : ℕ), Opn.Divides d m → d = (1 : ℕ) ∨ d = m

            Leaves ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m, with hnot : ¬∀ (d : ℕ), Opn.Divides d m → d = (1 : ℕ) ∨ d = m.

            Uses definitions Opn.Divides; library Nat The natural numbers, starting at zero. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. .

            Lean, line 16

                · have hnot : ¬ ∀ d : Nat, Opn.Divides d m → d = 1 ∨ d = m := fun h => hp ⟨hm, h⟩

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

         2. s1.s2.s2 obtain ∃ (d : ℕ), Opn.Divides d m ∧ d ≠ (1 : ℕ) ∧ d ≠ m

            Leaves ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m, with d : ℕ, c : ℕ, hc : m = d * c, hd1 : d ≠ (1 : ℕ), hdm : d ≠ m.

            Lean, line 18

                  obtain ⟨d, ⟨c, hc⟩, hd1, hdm⟩ := hnot

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

         3. s1.s2.hd0 have d ≠ (0 : ℕ)

            Leaves ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m, with hd0 : d ≠ (0 : ℕ).

            Uses library Nat.zero_mul.

            Lean, lines 19–22

                  have hd0 : d ≠ 0 := by
                    intro h
                    rw [h, Nat.zero_mul] at hc
                    omega

            targets/euclid-primes/nodes/infinitude-of-primes--h2/Proof.lean, lines 19–22 at b134abca6e5d ↗

         4. s1.s2.hdle have d ≤ m

            Leaves ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m, with hdle : d ≤ m.

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

            Lean, line 23

                  have hdle : d ≤ m := Nat.le_of_dvd (by omega) ⟨c, hc⟩

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

         5. s1.s2.s5 obtain ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p d

            Leaves ∃ (p : ℕ), Opn.IsPrime p ∧ Opn.Divides p m, with p : ℕ, hpp : Opn.IsPrime p, a : ℕ, ha : d = p * a.

            Lean, line 24

                  obtain ⟨p, hpp, a, ha⟩ := ih d (by omega) (by omega)

            targets/euclid-primes/nodes/infinitude-of-primes--h2/Proof.lean, line 24 at b134abca6e5d ↗

   Proof: targets/euclid-primes/nodes/infinitude-of-primes--h2/Proof.lean, lines 1–25 at b134abca6e5d.

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

3. infinitude-of-primes--h3 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 infinitude_of_primes__h3 : ∀ (n : ℕ),
     (∀ (k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial) →
       (∀ (m : ℕ), 2 ≤ m → ∃ p, Opn.IsPrime p ∧ Opn.Divides p m) →
         ∀ (d m : ℕ), Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := 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}:\ \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$

   For every natural number $n$, under the two inherited hypotheses (every $k$ with $0<k\le n$ divides $n!$, and every $m\ge 2$ has a prime divisor; the earlier holes' claims, which the conclusion does not use), any natural number $d$ dividing both $m$ and $m+1$ equals $1$. Divisibility is the problem's own Opn.Divides ($a\mid b$ when $b=a\cdot c$ for some natural $c$), prime is Opn.IsPrime, and $n!$ is Nat.factorial.

   Rendered from gloss/d667b839178a….md · Improve these words →

   Checked by the kernel — an outline of the proof attested in attestations/000036.json, merge commit f5880e7706a4.

   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. h1 have d ∣ m

      Leaves d = (1 : ℕ), with h1 : d ∣ m.

      Lean, line 13

        have h1 : d ∣ m := hdm

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

   2. h2 have d ∣ m + (1 : ℕ)

      Leaves d = (1 : ℕ), with h2 : d ∣ m + (1 : ℕ).

      Lean, line 14

        have h2 : d ∣ m + 1 := hdm1

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

   Proof: targets/euclid-primes/nodes/infinitude-of-primes--h3/Proof.lean, lines 1–15 at f5880e7706a4.

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

4. infinitude-of-primes--h4 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 infinitude_of_primes__h4 : ∀ (n : ℕ),
     (∀ (k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial) →
       (∀ (m : ℕ), 2 ≤ m → ∃ p, Opn.IsPrime p ∧ Opn.Divides p m) →
         (∀ (d m : ℕ), Opn.Divides d m → Opn.Divides d (m + 1) → d = 1) → ∀ (k : ℕ), 0 < k.factorial := 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}:\ \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!$

   For every natural number $n$, under the three inherited hypotheses (every $k$ with $0<k\le n$ divides $n!$; every $m\ge 2$ has a prime divisor; a common divisor of $m$ and $m+1$ is $1$; the earlier holes' claims, which the conclusion does not use), every factorial $k!$ is positive. Divisibility is the problem's own Opn.Divides, prime is Opn.IsPrime, and the factorial is Mathlib's Nat.factorial.

   Rendered from gloss/02043faa74f9….md · Improve these words →

   Checked by the kernel — an outline of the proof attested in attestations/000037.json, merge commit 7f81053778e5.

   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.

   Proof: targets/euclid-primes/nodes/infinitude-of-primes--h4/Proof.lean, lines 1–12 at 7f81053778e5.

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

5. infinitude-of-primes proved

   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.

   Checked by the kernel — an outline of the proof attested in 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 ↗

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

   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.

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

Correspondence