openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Number theory MSC2020 11A41

theorem

Why are there infinitely many primes?

ProvedFull statement

Full natural-number statement proved; the strict, non-strict, unbounded and infinite formulations are equivalent.

OpenMath assessment · decided Oct 10, 2026

Maintained research recordundergraduate backgroundChecked Oct 10, 2026Publication v3

Viewing pinned publication v3. 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

ProvedFull statement

Full natural-number statement proved; the strict, non-strict, unbounded and infinite formulations are equivalent.

OpenMath assessment · decided Oct 10, 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 10, 2026 · Recheck by Mar 30, 2027

Staff checked the equivalence under natural-number assumptions and retained exact source correspondence. Independent mathematical review remains pending.

Independent mathematical review: pending.

OpenMath · prime note

Proved

Source 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.

mathlib · infinitude of primes

Proved

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.

Formulations & supporting Claims

A Problem is the shared question. Its Claims record precise statements, their assumptions and how they relate to that question. Equivalent formulations share one answer.

Formulations

Primary formulation · theorem

A prime strictly above every bound →

For every natural number n, there exists a prime p with n < p.

The strict witness formulation states the canonical question.

Proved · cited result · Independent relationship review pending

Equivalent formulation · theorem

A prime at or above every bound →

For every natural number n, there exists a prime p with n ≤ p.

Apply this theorem at n + 1 to obtain n < p. Conversely n < p implies n ≤ p. This equivalence concerns the universal statements; a particular non-strict witness at n can equal n.

Proved · cited result · Independent relationship review pending

Equivalent formulation · theorem

The set of primes is unbounded →

The natural-number primes have no upper bound.

Unboundedness means that every natural-number bound has a larger prime. This is exactly the strict witness formulation.

Proved · cited result · Independent relationship review pending

Equivalent formulation · theorem

There are infinitely many primes →

The set of natural-number primes is infinite.

A finite set of natural numbers is bounded; a bounded set lies in a finite initial segment. Thus infinitude and unboundedness are equivalent here.

Proved · cited result · Independent relationship review pending

Supporting results

Supporting result · lemma

Characterizing a natural-number prime →

A natural number p is prime exactly when p ≥ 2 and every natural-number divisor m of p is either 1 or p.

This prerequisite supplies the divisibility contradiction in the factorial-plus-one proof. It is a supporting theorem, not another prime-infinitude Problem.

Proved · cited result · Independent relationship review pending

Literature & sources

Formalizations & evidence

Statement correspondence, execution, proof completeness, reproduction and mathematical review remain separate assessments.

staff linked

Pinned witness theorem

Nat.exists_infinite_primes ↗

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

staff linked

Pinned prime-divisor characterization

Nat.prime_def ↗

Source-level staff correspondence. A passing Run does not independently confirm informal/formal alignment.

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.

Formalize a prime strictly above every bound: all recent checks →

Related work

Insight · independent review pending

A prime divisor of factorial plus one →

The key move is not to find the next prime directly. Construct n! + 1, take one of its prime factors, and notice that any prime at most n would divide both n! and n! + 1. That impossible overlap supplies a prime beyond the alleged bound.

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

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 · 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
Publication v3 · history & checksums
Stable Problem ID
problem-prime-infinitude
Publication SHA-256
819f4d74fab5c02517a803fa5e9a7d1be638dab5f62dcbf7676bcc5c95e3fc1f
Published
2026-10-10T06:01:24.790345+00:00
Publication reason
Add cited resolution scope and consolidate equivalent prime formulations and supporting Claims; mathematical evidence and execution review remain distinct.
  1. v1 · publish · Sep 30, 2026

    Initial checked pilot publication; source attribution, rights, wording and coverage reviewed by OpenMath staff.

  2. 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.

  3. v3 · publish · Oct 10, 2026

    Add cited resolution scope and consolidate equivalent prime formulations and supporting Claims; mathematical evidence and execution review remain distinct.

  4. 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.

  5. v5 · publish · Oct 11, 2026

    Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.

  6. v6 · publish · Oct 12, 2026

    Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.

  7. v7 · publish · Oct 13, 2026

    Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.

  8. v8 · publish · Oct 14, 2026

    Reviewed reader correction: preserve assertion history, exact citations and scoped assessments; task evidence names its exact Claim target.

Download research recordReport a correction →