Problems / euclid-primes / infinitude-of-primes--h1
Every k with 1 <= k <= n divides n!
infinitude-of-primes--h1
proved
Hole dvd_fact of infinitude-of-primes (split by 20260912T110722Z-thisisanameforsure-partial.lean).
theorem infinitude_of_primes__h1 : ∀ (n k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial := 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 →
signed by thisisanameforsure · history For all natural numbers $n$ and $k$: if $0 < k$ and $k \le n$, then $k$ divides $n!$.
How it was proved
Proved by Proof.lean, checked by the kernel. Its attestation, 000034, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: 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.
s1obtaink ∣ n.factorialLeaves
Opn.Divides k n.factorial, withc : ℕ,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↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000034.json, merge commit a9f10904c037.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h1/Proof.lean, sha256 abb52c9e9aa1.import Defs.IsPrime import Mathlib.Tactic /-! Hole `dvd_fact` 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__h1 : ∀ (n k : ℕ), 0 < k → k ≤ n → Opn.Divides k n.factorial := by intro n k hk hkn -- Mathlib: a positive k ≤ n divides n!; `Opn.Divides` is the same ∃-statement. obtain ⟨c, hc⟩ := Nat.dvd_factorial hk hkn exact ⟨c, hc⟩
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).
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 `dvd_fact` 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__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
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$.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).
Rendered from targets/euclid-primes/nodes/infinitude-of-primes--h1/Statement.lean. Origin: skeleton-hole.
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000034.json, merge commit a9f10904c037.
Verdict pass, from attestations/000034.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/000034.json, merge commit a9f10904c037.
01f0b9db684e./-! 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. -/ /-- `n = k = 1`: 1 is positive and at most 1. -/ theorem witness : ∃ n k : Nat, 0 < k ∧ k ≤ n := ⟨1, 1, Nat.one_pos, Nat.le_refl 1⟩
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 →