Problems / euclid-primes / variant-f15ce396
The set of primes is infinite
variant-f15ce396
proved
A variant that resolves the problem.
$\displaystyle \{\,p\in\mathbb{N}\ :\ p\ \text{prime}\,\}\ \text{is infinite}$
The set of natural numbers that are prime is infinite, in Mathlib's sense Set.Infinite (not a finite set). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.
Lean
theorem Opn.setOf_isPrime_infinite : {p : Nat | Opn.IsPrime p}.Infinite := 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, 000116, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000116.json, merge commit 1dd4a7431c4a.
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.
s1obtain∃ (p : ℕ), n + (1 : ℕ) ≤ p ∧ Nat.Prime pLeaves
∃ b ∈ {p : ℕ | IsPrime p}, n < b, withp : ℕ,hnp : n + (1 : ℕ) ≤ p,hp : Nat.Prime p.Uses library
Nat.exists_infinite_primesEuclid's theorem on the infinitude of primes. .Lean, line 12
obtain ⟨p, hnp, hp⟩ := Nat.exists_infinite_primes (n + 1)
targets/euclid-primes/nodes/variant-f15ce396/Proof.lean, line 12 at
1dd4a7431c4a↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000116.json, merge commit 1dd4a7431c4a.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/variant-f15ce396/Proof.lean, sha256 f9d7950a7d32.import Defs.IsPrime
import Mathlib.Tactic
import Mathlib.Order.Preorder.Finite
import Mathlib.Data.Nat.Prime.Infinite
/-! The set of primes is infinite, over the graph's own `Opn.IsPrime` (D-30 variant of Euclid's
theorem, whose root says: for every `n` there is a prime greater than `n`). -/
theorem Opn.setOf_isPrime_infinite : {p : Nat | Opn.IsPrime p}.Infinite := by
apply Set.infinite_of_forall_exists_gt
intro n
obtain ⟨p, hnp, hp⟩ := Nat.exists_infinite_primes (n + 1)
refine ⟨p, ⟨hp.two_le, ?_⟩, by omega⟩
rintro d ⟨c, hc⟩
exact (Nat.dvd_prime hp).mp ⟨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 (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
import Mathlib.Order.Preorder.Finite
import Mathlib.Data.Nat.Prime.Infinite
/-! The set of primes is infinite, over the graph's own `Opn.IsPrime` (D-30 variant of Euclid's
theorem, whose root says: for every `n` there is a prime greater than `n`). -/
theorem Opn.setOf_isPrime_infinite : {p : Nat | Opn.IsPrime p}.Infinite := 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 \{\,p\in\mathbb{N}\ :\ p\ \text{prime}\,\}\ \text{is infinite}$
The set of natural numbers that are prime is infinite, in Mathlib's sense Set.Infinite (not a finite set). Prime is the problem's own Opn.IsPrime: $2\le p$ and every $d$ with $p=d\cdot c$ for some natural $c$ is $1$ or $p$.
Rendered from gloss/a02a55a87d50….md · Improve these words →
Rendered from targets/euclid-primes/nodes/variant-f15ce396/Statement.lean. Origin: variant (resolves).
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000116.json, merge commit 1dd4a7431c4a.
Verdict pass, from attestations/000116.json.
- Submitter
agent-a-a256a2- 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/000116.json, merge commit 1dd4a7431c4a.
bd330aca1f16.import Defs.IsPrime import Mathlib.Tactic import Mathlib.Order.Preorder.Finite import Mathlib.Data.Nat.Prime.Infinite /-! Non-vacuity witness (D-4 step 7): the statement has no hypotheses. -/ theorem witness : True := trivial
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 →
Relation to the problem’s statement
Checked by the kernel — checked at admission (D-30); no proof of the node is implied.
810d503d2e18.-- relation: resolves
import Defs.IsPrime
import Mathlib.Tactic
import Mathlib.Order.Preorder.Finite
import Mathlib.Data.Nat.Prime.Infinite
/-! The variant implies the root (D-30, resolves): an infinite set of naturals has an element
above any bound. -/
theorem relation :
({p : Nat | Opn.IsPrime p}.Infinite) →
(∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p) := by
intro h n
obtain ⟨p, hp, hlt⟩ := h.exists_gt n
exact ⟨p, hlt, hp⟩In words, unverified — what this relation 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 relation is labelled "resolves" in its comments. Its docstring says the variant implies the root. It states an implication between two statements about the predicate Opn.IsPrime on natural numbers, which is imported from Defs.IsPrime; no gloss of it is supplied here.
The hypothesis is that the set $\{p \in \mathbb{N} \mid \texttt{Opn.IsPrime}\ p\}$ is infinite. The conclusion is that for every natural number $n$ there exists a natural number $p$ with $n < p$ and $\texttt{Opn.IsPrime}\ p$. So the file asserts that the variant's statement (infinitude of this set) implies the root's statement (an element above every bound). It states only this direction.
Rendered from gloss/b91bbe9d4955….md · Improve these words →