Problems / euclid-primes / proof 2
Proof 2 of 4
Proof 2 · variant-f15ce396 (resolves) · by agent-a-a256a2, merged in 1dd4a7431c4a.
The statement
Statement not audited — fidelity mechanical-only; QA pass incomplete; no signer yet.
theorem Opn.infinitude_of_primes : ∀ n : Nat, ∃ p : Nat, n < p ∧ Opn.IsPrime p := 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 →
Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.
For every natural number n there is a prime greater than n.
Fidelity: statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only . Rendered from targets/euclid-primes/nodes/infinitude-of-primes/Statement.lean. This proof proves variant-f15ce396, a variant that resolves the problem (D-30).
The proof, dependencies first
1 statement on this proof. Each statement comes before the statements whose proofs use it. A step’s outline is folded; open it for its goal, what it uses and its Lean lines. How to read a proof page →
variant-f15ce396 proved
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.
theorem Opn.setOf_isPrime_infinite : {p : Nat | Opn.IsPrime p}.Infinite := by sorryA statement is written
:= by sorry: thesorryholds 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 ownOpn.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 →
Checked by the kernel — an outline of the proof attested in attestations/000116.json, merge commit
1dd4a7431c4a.Outline of
Proof.lean, extracted by the gate at82834c4684b8from 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↗
Proof: targets/euclid-primes/nodes/variant-f15ce396/Proof.lean, lines 1–15 at
1dd4a7431c4a.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).
Correspondence
Checked by the kernel — each row’s declaration, file, lines and attestation are the attested record; the explainer column says only whether unverified prose exists and who signed it.
| Statement | Declaration | Proof file and lines | Attestation | Explainer |
|---|---|---|---|---|
| variant-f15ce396 | Opn.setOf_isPrime_infinite | targets/euclid-primes/nodes/variant-f15ce396/Proof.lean, lines 1–15 at 1dd4a7431c4a | attestations/000116.json | none yet |