OpenMath · prime note
ProvedSource label: Known theorem in authored reference note
Source status date unavailable · Observed Oct 1, 2026
The cited source item and version only; this is not an independent OpenMath assessment.
Number theory MSC2020 11A41
QuestionWhy are there infinitely many primes?
Reported resolvedScope unassessed
Resolution scope has not been assessed in this publication.
OpenMath assessment · decided Oct 1, 2026
Viewing pinned publication v2. View the current publication →
Question & scope
For every natural number n, does there exist a prime p with n < p?
Natural numbers and ordinary primality. This strict formulation follows by applying the pinned at-or-above theorem at n + 1.
Question paraphrased by OpenMath. Use the cited source and locator for authoritative wording.
Research state
Reported resolvedScope unassessed
Resolution scope has not been assessed in this publication.
OpenMath assessment · decided Oct 1, 2026 · Elementary prime results · OpenMath staff
OpenMath decision · Elementary prime results
Known result
Established result supported by the cited note and pinned mathlib statement. The local exercise tests exact Lean inputs, not novelty.
OpenMath staff · Oct 1, 2026 · Recheck by Mar 30, 2027
Wording, natural-number assumptions and pinned source correspondence checked by staff. Independent mathematical review remains pending.
Independent mathematical review: pending.
Source label: Proved declaration Nat.exists_infinite_primes
Source status date unavailable · Observed Oct 1, 2026
The cited source item and version only; this is not an independent OpenMath assessment.
Literature & sources
OpenMath source note ↗
Original exposition under CC BY 4.0; exact spans and hashes retained.
Formalizations & evidence
Statement correspondence, execution, proof completeness, reproduction and mathematical review remain separate assessments.
staff linked
Pinned witness theorem
Source-level staff correspondence. A passing Run does not independently confirm informal/formal alignment.
Exact commit 32d24245c7a1 · Checked Oct 1, 2026
disputed
Disputed direct strict-bound mapping
Nat.exists_infinite_primes → n < p without shifting n ↗
Treating the returned n ≤ p as a direct proof of n < p is invalid. The recorded broken input exposes this mismatch; applying the theorem at n + 1 repairs the route.
Exact commit 32d24245c7a1 · Checked Oct 1, 2026
Recorded verification evidence
Checks concern exact versioned inputs from the linked Tasks. The latest six recorded executions are shown here; their proof policy, correspondence, reproduction and review are assessed separately. Staff repeat instructions are included in the research record export.
- Strict-bound corollary typechecksHistorical local reference observation · Independent reproduction pending
- Off-by-one proof attempt failsHistorical local reference observation · Independent reproduction pending
Formalize a prime strictly above every bound: all recent checks →
Provenance & coverage
Published after staff preview and source checks. This page covers the cited items; it does not represent a complete list of problems or a literature-wide review.
- No exhaustive literature or source-list coverage.
- Independent mathematical assessment has not been performed.
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
1 cited entry · 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
Publication v2 · history & checksums
- Stable Problem ID
- problem-prime-infinitude
- Publication SHA-256
- 55f3cdfbbfa0a6507daaccd6c7f5951c2e256137cd97c02c542970e2d55de232
- Published
- 2026-09-30T20:35:54.398381+00:00
- Publication reason
- Refine the maintained cluster: link a distinct prime-divisor prerequisite; retain the strict-bound exercise as a Task on the infinitude Problem.
- v1 · publish · Sep 30, 2026
Initial checked pilot publication; source attribution, rights, wording and coverage reviewed by OpenMath staff.
- v2 · publish · 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.
- v3 · publish · Oct 10, 2026
Add cited resolution scope and consolidate equivalent prime formulations and supporting Claims; mathematical evidence and execution review remain distinct.
- v4 · publish · 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.
- v5 · publish · Oct 11, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- v6 · publish · Oct 12, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- v7 · publish · Oct 13, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.
- v8 · publish · Oct 14, 2026
Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.