Problems / euclid-primes / variant-6e71b160
Primes at least 100, the bound written as p = 100 + k
variant-6e71b160
abandoned
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\ \bigl(\exists k\in\mathbb{N},\ p=100+k\bigr)\ \wedge\ p\ \text{prime}$
For every natural number $n$ there is a prime $p>n$ that is at least $100$, the bound being written as "$p=100+k$ for some natural number $k$" rather than as $100\le p$. 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_ge_hundred : ∀ n : Nat, ∃ p : Nat, n < p ∧ (∃ k : Nat, p = 100 + k) ∧ 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 is being proved
Abandoned.
What is known
Work on it
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-6e71b160».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`. The bound is inclusive and is written in the style of `Opn.Divides`, as `∃ k, p = 100 + k`. A consequence of the root `Opn.infinitude_of_primes` (apply it at `max n 100`), which this node declares as a dependency. -/ theorem Opn.infinitude_of_primes_ge_hundred : ∀ n : Nat, ∃ p : Nat, n < p ∧ (∃ k : Nat, p = 100 + k) ∧ 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\ \bigl(\exists k\in\mathbb{N},\ p=100+k\bigr)\ \wedge\ p\ \text{prime}$
For every natural number $n$ there is a prime $p>n$ that is at least $100$, the bound being written as "$p=100+k$ for some natural number $k$" rather than as $100\le p$. 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/e3855f51d25d….md · Improve these words →
Rendered from targets/euclid-primes/nodes/variant-6e71b160/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.
Witness
Not checked — no run on this page records step 7 passing for it.
d458c07694a0.import Nodes.«variant-6e71b160».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 →
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).