Problem · reference example
Why are there infinitely many primes?
A known theorem shown with its source, related formal statements, proof idea, and a bounded follow-up task.
Statement
A source-linked formulation of the known theorem.
The pinned mathlib declaration Nat.exists_infinite_primes gives a formal witness statement. Its exact source and the informal note are available below.
Related claims
Links describe candidate or staff-curated correspondences. Each claim retains its own evidence status.
| Claim | Lean declaration | Source link |
|---|---|---|
| A prime at or above every bound | Nat.exists_infinite_primes | Staff linked |
| The set of primes is unbounded | Nat.not_bddAbove_setOf_prime | Possible match |
| There are infinitely many primes | Nat.infinite_setOf_prime | Possible match |
| A prime strictly above every bound | OpenMath.Phase0.exists_prime_strictly_above | Staff linked |
Proof idea
The key move is not to find the next prime directly. Construct n! + 1, take one of its prime factors, and notice that any prime at most n would divide both n! and n! + 1. That impossible overlap supplies a prime beyond the alleged bound.
Nat.exists_infinite_primes and factorial proofMathlib: infinitude of primes · lines 31–42Follow-up task
Formalize a prime strictly above every bound
A Lean declaration for ∀ n, ∃ p, n < p ∧ Nat.Prime p, plus a short source-grounded explanation.