Claim · version 1
The set of primes is unbounded
A mathematical statement linked to a source passage and a Lean declaration. The correspondence has its own review status.
Possible source match
Statement and Lean representation
There is no upper bound on natural-number primes.
Nat.not_bddAbove_setOf_prime
¬BddAbove { p | Nat.Prime p }
¬BddAbove { 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
- Possible match; unresolved
- Independent reproduction
- Not yet reproduced
- Mathematical review
- Independent review pending
Proof outline
A bound would contradict the witness theorem
- Assume an upper bound.
- Apply the witness theorem beyond that bound.
This outline is source-linked and awaits independent mathematical review.