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 3
The set of primes is unbounded
Statement
The natural-number primes have no upper bound.
Assumptions
- Natural numbers
- Ordinary primality
Scope
Natural-number primes with their usual order.
Evidence
Source reports
Proved
Known theorem in authored reference note ↗
The cited source item and version only; this is not an independent OpenMath assessment.
OpenMath · prime note · notes/primes.md lines 9–15, 21–29 →
Observed Oct 1, 2026
Connections
In this problem · publication v5 · Selected context
Why are there infinitely many primes? →
Equivalent formulation · Proved
Unboundedness means that every natural-number bound has a larger prime. This is exactly the strict witness formulation.
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.
In this problem · publication v8
Why are there infinitely many primes? →
Equivalent formulation · Proved
Unboundedness means that every natural-number bound has a larger prime. This is exactly the strict witness formulation.
Unboundedness says that no natural-number bound contains every prime.
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
OpenMath · prime note →
- notes/primes.md lines 9–15, 21–29 → · Original passage ↗
Recorded wording
For every natural number n, does there exist a prime p with n < p?
paraphrase · Licensed source links and exact source spans; attribution retained.
OpenMath staff · Revision a640f3adfa536da0
mathlib · infinitude of primes →
- Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42 → · Original passage ↗
Recorded wording
For every natural number n, does there exist a prime p with 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 · 2
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Known theorem in authored reference note ↗
The cited source item and version only; this is not an independent OpenMath assessment.
Observed Oct 1, 2026 · Source passage →
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-primes-unbounded
- Statement version
- 3
- SHA-256
- 00e896e8149ca86184a50e3f58cadb5a6d4db874568f10051f9cb93acc898a54