Reading source record 32d24245c7a12ded17325299fd41d412022cd3fe. View default cited record →
Natural-number prime statements
2 cited passages ↓1 problem ↓Record 32d24245c7a12ded17325299fd41d412022cd3fe ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
For each natural number n, there is a prime p satisfying n ≤ p.
Passage ID: prime-at-or-above-bound:entry:0:v1
Source item: Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42
Source record: mathlib-prime-infinite@32d24245c7a12ded17325299fd41d412022cd3fe
For every natural number n, does there exist a prime p with n < p?
Passage ID: prime-infinitude:entry:1:v1
Source item: Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42
Source record: mathlib-prime-infinite@32d24245c7a12ded17325299fd41d412022cd3fe
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v8
Source assessment
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 assessment
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 assessment
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 assessment
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
Question
Why are there infinitely many primes?
Further reading
Inspect the formal statement, assumptions and reported checks.
mathlib contributors
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
mathlib · infinitude of primes
Licensed source links and exact source spans; attribution retained.
Source terms ↗