Claim · version 1
There are infinitely many primes
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
The set of natural-number primes is infinite.
Nat.infinite_setOf_prime
{ p | Nat.Prime p }.Infinite
{ p | Nat.Prime p }.Infinite
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
Unbounded natural-number sets are infinite
- Use the unbounded-set formulation.
- Apply the pinned mathlib set-theoretic result.
This outline is source-linked and awaits independent mathematical review.