Proved
Proved declaration Nat.exists_infinite_primes ↗
The cited source item and version only; this is not an independent OpenMath assessment.
mathlib · infinitude of primes · Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42 →
Observed Oct 1, 2026
Theorem · version 2
A prime at or above every bound
Earlier version 2. View current version 3 →
Statement
For every natural number n, there exists a prime p with n ≤ p.
Assumptions
- Natural numbers
- Ordinary primality
Scope
Same natural-number domain as the strict formulation.
Evidence
Source reports
Formal proofs
Pinned witness theorem ↗
OpenMath links the informal and formal statements; independent correspondence review remains separate. A passing Run does not independently confirm informal/formal alignment.
Statement match: Linked by OpenMath · independent review separate · checked Oct 1, 2026
Declaration & revision
Nat.exists_infinite_primesCommit 32d24245c7a12ded17325299fd41d412022cd3fe
Connections
In this problem · publication v3
Why are there infinitely many primes? →
Equivalent formulation · Proved
Apply this theorem at n + 1 to obtain n < p. Conversely n < p implies n ≤ p. This equivalence concerns the universal statements; a particular non-strict witness at n can equal n.
Relationship not independently reviewed. This concerns its use in this problem.
Formalize a prime strictly above every bound → · Related problem work; no execution evidence for this statement is asserted.
Sources
mathlib · infinitude of primes →
- Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42 → · Original passage ↗
Recorded wording
For each natural number n, there is a prime p satisfying n ≤ p.
paraphrase · Licensed source links and exact source spans; attribution retained.
mathlib contributors · Revision 32d24245c7a12ded17325299fd41d412022cd3fe
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Proved declaration Nat.exists_infinite_primes ↗
The cited source item and version only; this is not an independent OpenMath assessment.
Observed Oct 1, 2026 · Source passage →
Record details
- Claim ID
- claim-prime-above-bound
- Statement version
- 2
- SHA-256
- 6de133f4d3042f6f27522b6c69b6101939395a3c5713713548c95974fe1a3061