Claim · version 1
A prime at or 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.
Nat.exists_infinite_primes
∀ 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
- Upstream declaration pinned
- Statement alignment
- Linked by OpenMath staff; review pending
- Independent reproduction
- Not yet reproduced
- Mathematical review
- Independent review pending
Proof outline
A prime factor of n! + 1
- Choose a prime factor p of n! + 1.
- If p ≤ n, then p divides n!.
- It would then divide the difference (n! + 1) - n! = 1, a contradiction.
- Therefore p ≥ n.
This outline is source-linked and awaits independent mathematical review.