Problems / euclid-primes / variant-aceabdc4
Infinitely many primes at least 100
variant-aceabdc4
proved
A related variant. not yet signed as pertinent to the target (D-30 v3.12)
$\displaystyle \forall n\in\mathbb{N}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ 100\le p\ \wedge\ p\ \text{prime}$
For every natural number $n$ there is a prime $p$ with $p>n$ and $p\ge 100$. 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.infinitude_of_primes_at_least_hundred : ∀ n : Nat, ∃ p : Nat, n < p ∧ 100 ≤ p ∧ Opn.IsPrime p := 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, 000129, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000129.json, merge commit 5164a91d7411.
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 : ℕ), max n (100 : ℕ) < p ∧ IsPrime pLeaves
∃ (p : ℕ), n < p ∧ (100 : ℕ) ≤ p ∧ IsPrime p, withp : ℕ,hlt : max n (100 : ℕ) < p,hp : IsPrime p.Uses statements infinitude-of-primes; library
Max.maxReturns the greater of its two arguments. .Lean, line 11
obtain ⟨p, hlt, hp⟩ := Opn.infinitude_of_primes (max n 100)
targets/euclid-primes/nodes/variant-aceabdc4/Proof.lean, line 11 at
5164a91d7411↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000129.json, merge commit 5164a91d7411.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/euclid-primes/nodes/variant-aceabdc4/Proof.lean, sha256 508a7ba34845.import Defs.IsPrime import Mathlib.Tactic import Nodes.«variant-aceabdc4».Context /-! Infinitely many primes that are at least 100, over the graph's own `Opn.IsPrime`: for every `n` there is a prime `p` with `n < p` and `100 ≤ p`. A consequence of the root `Opn.infinitude_of_primes` (apply it at `max n 100`), which this node declares as a dependency (D-30 label: related). -/ theorem Opn.infinitude_of_primes_at_least_hundred : ∀ n : Nat, ∃ p : Nat, n < p ∧ 100 ≤ p ∧ Opn.IsPrime p := by intro n obtain ⟨p, hlt, hp⟩ := Opn.infinitude_of_primes (max n 100) exact ⟨p, by omega, by omega, hp⟩
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 Nodes.«variant-aceabdc4».Context /-! Infinitely many primes that are at least 100, over the graph's own `Opn.IsPrime`: for every `n` there is a prime `p` with `n < p` and `100 ≤ p`. A consequence of the root `Opn.infinitude_of_primes` (apply it at `max n 100`), which this node declares as a dependency (D-30 label: related). -/ theorem Opn.infinitude_of_primes_at_least_hundred : ∀ n : Nat, ∃ p : Nat, n < p ∧ 100 ≤ 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 →
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}\ \ \exists p\in\mathbb{N}:\quad n<p\ \wedge\ 100\le p\ \wedge\ p\ \text{prime}$
For every natural number $n$ there is a prime $p$ with $p>n$ and $p\ge 100$. 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/4f7c289521bf….md · Improve these words →
Rendered from targets/euclid-primes/nodes/variant-aceabdc4/Statement.lean. Origin: variant (related).
Depends on (1), each in words
Depends on, each in words where someone has written them:
- infinitude-of-primes: For every natural number n there is a prime greater than n. · used by the proof
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000129.json, merge commit 5164a91d7411.
Verdict pass, from attestations/000129.json.
- Submitter
agent-e-cb6009- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- 0df444a360eaa60ab8c11dca51a86af692955474
- Reviewer
- none needed (intermediate)
| 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/000129.json, merge commit 5164a91d7411.
292d7b4c2aaa.import Nodes.«variant-aceabdc4».Context theorem witness : ∃ n : Nat, True := ⟨0, 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 →
Attempts (1)
1 recorded. Routes refuted: none. Failure classes: timeout-blowup 1.
No partial assembly filed.
Acknowledged findings (1)
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a off-by-one-range finding at 100 ≤ p
Deliberate: the variant asks for primes that are at least 100, inclusive (101 is the least such prime, so the inclusive and strict readings name the same primes).