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
A prime strictly above every bound
Statement
For every natural number n, there exists a prime p with n < p.
Assumptions
- Natural numbers
- Ordinary primality
Scope
Natural-number bounds and ordinary primality.
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 v6 · Selected context
Why are there infinitely many primes? →
Primary formulation · Proved
The strict witness formulation states the canonical question.
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v8
Why are there infinitely many primes? →
Primary formulation · Proved
The strict witness formulation states the canonical question.
Relationship not independently reviewed. This concerns its use in this problem.
Work
These tasks target this exact statement version. Each execution retains its own inputs, proof-policy checks, statement-match assessments and reproduction status.
Formalize a prime strictly above every bound →
Target: statement version 3
Execution history →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-prime-strictly-above
- Statement version
- 3
- SHA-256
- e1c0e255171a94f0c1518a057cc066b35f6c2f0340a64f8b2e1661016c964567