Number theory · Theorem
For every natural number n, does there exist a prime p with n < p?
Earlier version 8 of this page. View current →
Full natural-number statement proved; the strict, non-strict, unbounded and infinite formulations are equivalent.
Natural numbers and ordinary primality. The question asks for a prime strictly larger than any specified bound.
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.
Precise statement · Strict and non-strict formal statement correspondence
Natural numbers and ordinary primality. This strict formulation follows by applying the pinned at-or-above theorem at n + 1.
Question paraphrased by OpenMath. Original wording is available in the sources.
Figures and explorable examples. Selecting a statement opens its exact wording.
Each n! + 1 has a smallest prime factor larger than n, exactly as the proof predicts; sometimes n! + 1 is itself prime.
| n | n! + 1 | smallest prime factor p | as p × cofactor |
|---|---|---|---|
| 1 | 2 | 2 | prime |
| 2 | 3 | 3 | prime |
| 3 | 7 | 7 | prime |
| 4 | 25 | 5 | 5 × 5 |
| 5 | 121 | 11 | 11 × 11 |
| 6 | 721 | 7 | 7 × 103 |
| 7 | 5,041 | 71 | 71 × 71 |
| 8 | 40,321 | 61 | 61 × 661 |
| 9 | 362,881 | 19 | 19 × 19,099 |
| 10 | 3,628,801 | 11 | 11 × 329,891 |
| 11 | 39,916,801 | 39,916,801 | prime |
| 12 | 479,001,601 | 13 | 13 × 36,846,277 |
Twelve instances of the argument, computed exactly. The theorem for every n is the linked statement and its formal proof.
Natural-number bounds and ordinary primality.
Theorem · Primary formulation
ProvedOpenMath staffA prime strictly above every bound
The strict witness formulation states the canonical question.
Natural-number bounds and ordinary primality.
Same natural-number domain as the strict formulation.
Theorem · Equivalent formulation
Provedmathlib contributorsA prime at or above every bound
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.
Same natural-number domain as the strict formulation.
Natural-number primes with their usual order.
Theorem · Equivalent formulation
ProvedOpenMath staffThe set of primes is unbounded
Unboundedness means that every natural-number bound has a larger prime. This is exactly the strict witness formulation.
Unboundedness says that no natural-number bound contains every prime.
Natural-number primes with their usual order.
Natural numbers; no claim of this equivalence for arbitrary ordered sets.
Theorem · Equivalent formulation
ProvedOpenMath staffThere are infinitely many primes
A finite set of natural numbers is bounded; a bounded set lies in a finite initial segment. Thus infinitude and unboundedness are equivalent here.
A bounded set of natural numbers is finite, so infinitude and unboundedness agree.
Natural numbers; no claim of this equivalence for arbitrary ordered sets.
Natural-number divisibility and ordinary primality.
Lemma · Supporting result
Provedmathlib contributorsCharacterizing a natural-number prime
This prerequisite supplies the divisibility contradiction in the factorial-plus-one proof. It is a supporting theorem, not another prime-infinitude Problem.
This characterizes primality; it is not another infinitude result.
Natural-number divisibility and ordinary primality.
| Literature | Status OpenMath assessment · Oct 10, 2026.
|
|---|---|
| Formal | |
| Computation | |
| Review | Not yet reviewed OpenMath assessment: Established result supported by the cited note and pinned mathlib statement. The local exercise tests exact Lean inputs, not novelty. Staff checked the equivalence under natural-number assumptions and retained exact source correspondence. Independent mathematical review remains pending. Elementary prime results · OpenMath staff · assessed Oct 10, 2026 · review due Mar 30, 2027 |
OpenMath links the informal and formal statements; independent correspondence review remains separate. A passing Run does not independently confirm informal/formal alignment.
Statement match: Linked by OpenMath · independent review separate · checked Oct 1, 2026
Nat.exists_infinite_primesCommit 32d24245c7a12ded17325299fd41d412022cd3fe
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.
Statement match: Correspondence disputed · checked Oct 1, 2026
Nat.exists_infinite_primes → n < p without shifting nCommit 32d24245c7a12ded17325299fd41d412022cd3fe
OpenMath links the informal and formal statements; independent correspondence review remains separate. A passing Run does not independently confirm informal/formal alignment.
Statement match: Linked by OpenMath · independent review separate · checked Oct 1, 2026
Nat.prime_defCommit 32d24245c7a12ded17325299fd41d412022cd3fe
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Check the shifted-bound proof and inspect the failed unshifted route with the approved Lean recipe.
Target: A prime strictly above every bound →
View runs →Loading task runs…
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Read the setting and notation before comparing the results.
Inspect the formal statement, assumptions and reported checks.
OpenMath staff
Original exposition under CC BY 4.0; exact spans and hashes retained.
mathlib contributors
mathlib contributors
Selected literature; source observations and coverage limits are retained in the publication details.
The OpenMath note explains the classical infinitude argument. Mathlib contributors provide the linked formal theorems and prime definitions.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.
Up to six recent runs across the linked tasks. Each check concerns its own versioned inputs, rather than this entire problem record. A passing execution does not establish other statements, statement correspondence or independent reproduction.
Historical local reference observation · independent reproduction pending
Historical local reference observation · independent reproduction pending