Open Proof Network

Problems / euclid-primes / infinitude-of-primes--h3

Only 1 divides two consecutive numbers

infinitude-of-primes--h3

proved

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

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

unverified · history

Lean
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
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, 000036, records the gate’s run.

The proof step by step (outline)

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

The proof in Lean (Proof.lean)

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

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--h3/Proof.lean, sha256 f2f2f2613dbc.
import Defs.IsPrime
import Mathlib.Tactic

/-! Hole `dvd_consecutive` 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__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
  intro _ _ _ d m hdm hdm1
  -- `Opn.Divides` unfolds to core `∣`; d ∣ m and d ∣ m + 1 give d ∣ 1.
  have h1 : d ∣ m := hdm
  have h2 : d ∣ m + 1 := hdm1
  exact Nat.dvd_one.mp ((Nat.dvd_add_right h1).mp h2)

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

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

Record

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

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Defs.IsPrime
import Mathlib.Tactic

/-! Hole `dvd_consecutive` 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__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 →

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

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000036.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/000036.json, merge commit f5880e7706a4.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h3/Witness.lean, sha256 94ec98466d7f.
/-! 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.
-/

/-- Every number at least 2 has a prime divisor, over the graph's own definitions. Lean core
only: strong induction, and the classical extraction of a non-trivial divisor when `m` is not
prime. -/
theorem exists_prime_divisor : ∀ m : Nat, 2 ≤ m → ∃ p, Opn.IsPrime p ∧ Opn.Divides p m := by
  intro 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 hex : ∃ d, Opn.Divides d m ∧ d ≠ 1 ∧ d ≠ m :=
        Classical.byContradiction fun hc =>
          hp ⟨hm, fun d hd =>
            Classical.byContradiction fun hne =>
              hc ⟨d, hd, fun h => hne (Or.inl h), fun h => hne (Or.inr h)⟩⟩
      obtain ⟨d, ⟨c, hdc⟩, hd1, hdm⟩ := hex
      have hd0 : d ≠ 0 := by
        intro h
        rw [h, Nat.zero_mul] at hdc
        omega
      have hdle : d ≤ m := Nat.le_of_dvd (by omega) ⟨c, hdc⟩
      have hd2 : 2 ≤ d := by omega
      have hdlt : d < m := by omega
      obtain ⟨p, hpp, a, hpa⟩ := ih d hdlt hd2
      exact ⟨p, hpp, ⟨a * c, by rw [hdc, hpa, Nat.mul_assoc]⟩⟩

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

In words, unverified — what this witness 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 file proves an auxiliary theorem, exists_prime_divisor. It states that for every natural number $m$ with $2 \le m$ there is a $p$ such that Opn.IsPrime p and Opn.Divides p m. These are the graph's own notions of primality and divisibility, taken from an import whose gloss is not given here. Informally: every natural number $m \ge 2$ has a prime divisor $p$.

The theorem witness asserts that there exist natural numbers $n, d, m$ satisfying four conditions together:

  • For every natural number $k$ with $0 < k$ and $k \le n$, $k$ divides $n!$ (in the sense of Opn.Divides).
  • For every natural number $m$ with $2 \le m$ there is a $p$ with Opn.IsPrime p and Opn.Divides p m. Here $m$ is a fresh universally quantified variable, separate from the existentially chosen $m$.
  • $d$ divides $m$.
  • $d$ divides $m + 1$.

The file exhibits $n = 0$, $d = 1$, $m = 1$. The first condition holds vacuously, since no $k$ satisfies both $0 < k$ and $k \le 0$. The second condition is discharged by exists_prime_divisor. The last two say that $1$ divides $1$ and $1$ divides $2$.

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

How to read this page

How to read a statement’s page →