OpenMath · prime note ↗
Known theorem in authored reference note · observed Oct 1, 2026
Source status date unavailable · observed Oct 1, 2026
The cited source item and version only; this is not an independent OpenMath assessment.
Publication v7
Record details
Why are there infinitely many primes? →Coverage & review
- No exhaustive literature or source-list coverage.
- Independent mathematical assessment has not been performed.
General status observations
mathlib · infinitude of primes ↗
Proved declaration Nat.exists_infinite_primes · observed Oct 1, 2026
Source status date unavailable · observed Oct 1, 2026
The cited source item and version only; this is not an independent OpenMath assessment.
Source identities & rights
OpenMath · prime note ↗
OpenMath staff · full-text · CC-BY-4.0
Licensed source links and exact source spans; attribution retained. Rights / source terms
1 cited entry · exact source identity
- Version
- openmath-prime-note@a640f3adfa536da0
- Revision
- a640f3adfa536da0
- Content SHA-256
- a640f3adfa536da0fb792b52610d9d9d56540fbeb430df766667a4ff65b8b49f
- Source update
- 2026-09-26
- Observed
- 2026-10-01
- Check cadence
- 180 days
- notes/primes.md lines 9–15, 21–29 ↗
prime-infinitude:entry:0:v1
mathlib · infinitude of primes ↗
mathlib contributors · licensed-excerpt · Apache-2.0
Licensed source links and exact source spans; attribution retained. Rights / source terms
2 cited entries · exact source identity
- Version
- mathlib-prime-infinite@32d24245c7a12ded17325299fd41d412022cd3fe
- Revision
- 32d24245c7a12ded17325299fd41d412022cd3fe
- Content SHA-256
- 4d7a663d097dc291c3c3e55d097c7c5d0adfc7cb215c4700917f09c0acfbd527
- Source update
- Unavailable
- Observed
- 2026-10-01
- Check cadence
- 180 days
- Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42 ↗
prime-infinitude:entry:1:v1 - Mathlib/Data/Nat/Prime/Infinite.lean lines 31–42 ↗
prime-at-or-above-bound:entry:0:v1
mathlib · natural-number prime definitions ↗
mathlib contributors · licensed-excerpt · Apache-2.0
Licensed source links and exact source spans; attribution retained. Rights / source terms
1 cited entry · exact source identity
- Version
- mathlib-prime-defs@32d24245c7a12ded17325299fd41d412022cd3fe
- Revision
- 32d24245c7a12ded17325299fd41d412022cd3fe
- Content SHA-256
- ed1f1384e13ab35eb5bf0b4d0dba1572dcb927998557e9b3f6565cda55bc3e47
- Source update
- Unavailable
- Observed
- 2026-10-01
- Check cadence
- 180 days
- Mathlib/Data/Nat/Prime/Defs.lean lines 97–105 ↗
prime-divisor-characterization:entry:v1
Publication history
- Problem ID
- problem-prime-infinitude
- Publication checksum
- 2a54870eae9c7203c97a8820c16e69f0a2b4b31d9c281ba45a84e863207b1106
- Published
- 2026-10-13T19:35:04.009564+00:00
- Publication reason
- Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 1 · Sep 30, 2026
Initial checked pilot publication; source attribution, rights, wording and coverage reviewed by OpenMath staff.
- Version 2 · Sep 30, 2026
Refine the maintained cluster: link a distinct prime-divisor prerequisite; retain the strict-bound exercise as a Task on the infinitude Problem.
- Version 3 · Oct 10, 2026
Add cited resolution scope and consolidate equivalent prime formulations and supporting Claims; mathematical evidence and execution review remain distinct.
- Version 4 · Oct 11, 2026
Publish checked pilot curation with canonical Claims and scoped progress; preserve exact source revisions, assumptions, coverage limits and historical publications. External artifacts and OpenMath execution remain distinct.
- Version 5 · Oct 11, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 6 · Oct 12, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 7 · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- Version 8 · Oct 14, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.