Open Proof Network

Problems / euclid-primes / infinitude-of-primes--h2

Every m >= 2 has a prime divisor

infinitude-of-primes--h2

proved

Hole prime_divisor of infinitude-of-primes (split by 20260912T110722Z-thisisanameforsure-partial.lean).

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

unverified · history The theorem infinitude_of_primes__h2 asserts the following.

Explain this →

How it was proved

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

The proof step by step (outline)

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

The proof in Lean (Proof.lean)

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

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--h2/Proof.lean, sha256 55a53a1c45b0.
import Defs.IsPrime
import Mathlib.Tactic

/-! Hole `prime_divisor` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

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
  intro _ _ m
  -- Strong induction on m: m is prime, or it has a proper divisor d with 2 ≤ d < m.
  induction m using Nat.strongRecOn with
  | _ 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]⟩

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 (2 versions)

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

/-! Hole `prime_divisor` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

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

Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h2/Statement.lean. Origin: skeleton-hole.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000035.json, merge commit b134abca6e5d.

Verdict pass, from attestations/000035.json.

Submitter
not recorded
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/000035.json, merge commit b134abca6e5d.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h2/Witness.lean, sha256 19919408a56f.
/-! Non-vacuity witness (D-4 step 7) for a hole of the merged skeleton (D-12 #5, D-29).

The expected type is the hole's hypotheses, closed over the variables they mention (F01-R3):
a hole that inherits earlier lemmas as hypotheses can only be witnessed by discharging them, so
this file proves what it must. Lean core only — no Mathlib name appears — although the
statement's environment offers Mathlib, because a core proof is checkable anywhere the toolchain
is and cannot drift with a Mathlib rename.
-/

/-- With `n = 0` the first hypothesis is vacuous: no `k` is both positive and at most 0. -/
theorem witness : ∃ n m : Nat,
    (∀ k : Nat, 0 < k → k ≤ n → Opn.Divides k n.factorial) ∧ 2 ≤ m :=
  ⟨0, 2, fun _ hk hle => absurd hk (by omega), by omega⟩

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 →

How to read this page

How to read a statement’s page →