Problems / euclid-primes / infinitude-of-primes--h4
The factorial is positive
infinitude-of-primes--h4
proved
Hole fact_pos 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\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.
Lean
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
sorryWhy 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, 000037, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: 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.
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000037.json, merge commit 7f81053778e5.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h4/Proof.lean, sha256 cd3b591baea6.import Defs.IsPrime
import Mathlib.Tactic
/-! Hole `fact_pos` 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__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
intro _ _ _ _ k
exact Nat.factorial_pos kWhat 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).
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 `fact_pos` 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__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
sorryA 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 →
Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h4/Statement.lean. Origin: skeleton-hole.
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000037.json, merge commit 7f81053778e5.
Verdict pass, from attestations/000037.json.
- Submitter
- not recorded
- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- 0df444a360eaa60ab8c11dca51a86af692955474
- Reviewer
- thisisanameforsure
| Step | Check | Result |
|---|---|---|
| 1 | toolchain | pass |
| 2 | paths | pass |
| 4 | kernel-replay | pass |
| 5 | axioms | pass |
| 6 | hazards | pass |
| 7 | witness | pass |
| 8 | deps | pass |
Witness
Checked by the kernel — step 7 passed in the run its attestation records: attestations/000037.json, merge commit 7f81053778e5.
8f7d6489ae44./-! 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]⟩⟩
/-- Nothing but 1 divides two consecutive numbers. `Opn.Divides d m` is core `d ∣ m` written
out, so the core divisibility lemmas apply to it definitionally. -/
theorem dvd_consecutive : ∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1 := by
intro d m hdm hdm1
have h1 : d ∣ m := hdm
have h2 : d ∣ (m + 1) := hdm1
have h3 : d ∣ 1 := (Nat.dvd_add_right h1).mp h2
exact Nat.dvd_one.mp h3
/-- With `n = 0` the first hypothesis is vacuous: no `k` is both positive and at most 0. -/
theorem witness : ∃ n k : Nat,
(∀ j : Nat, 0 < j → j ≤ n → Opn.Divides j n.factorial) ∧
(∀ m : Nat, 2 ≤ m → ∃ p, Opn.IsPrime p ∧ Opn.Divides p m) ∧
(∀ d m : Nat, Opn.Divides d m → Opn.Divides d (m + 1) → d = 1) :=
⟨0, 0, fun _ hk hle => absurd hk (by omega), exists_prime_divisor, dvd_consecutive⟩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 →