Claim · version 1
A prime strictly above every bound
A mathematical statement linked to a source passage and a Lean declaration. The correspondence has its own review status.
Staff-linked source match
Statement and Lean representation
For every natural number n, some prime p satisfies n < p.
OpenMath.Phase0.exists_prime_strictly_above
∀ n : ℕ, ∃ p, n < p ∧ Nat.Prime p
∀ n : ℕ, ∃ p, n < p ∧ Nat.Prime p
A Lean check concerns the formal statement. The match to the cited wording awaits independent review.
Evidence
The four dimensions below have distinct meanings and do not inherit one another's status.
- Lean check
- Lean typecheck passed locally
- Statement alignment
- Linked by OpenMath staff; review pending
- Independent reproduction
- Not yet reproduced
- Mathematical review
- Independent review pending
Proof outline
Shift the bound by one
- Ask the existing theorem for a prime p ≥ n + 1.
- Conclude p > n.
This outline is source-linked and awaits independent mathematical review.