Source · OpenMath-authored note
Prime numbers do not run out
The cited note behind the theorem statement, proof idea, related formulations, and sample task. Line anchors identify exact passages in this version.
CC BY 4.0Independent review pending
Source text
1# Prime numbers do not run out
2
3This OpenMath-authored note is a Phase 0 reference source, not a survey of the literature or a new mathematical result. This note is available under CC BY 4.0; independent mathematical review is pending.
4
5## Definition
6
7A natural number is prime when it is at least two and has no positive divisors other than one and itself. Mathlib represents this as `Nat.Prime`; the representation is implemented using irreducibility and has an equivalent divisor characterization.
8
9## A prime beyond any bound
10
11For every natural number `n`, there is a prime `p` with `n ≤ p`. This is the formulation of Euclid's theorem used by `Nat.exists_infinite_primes` in the pinned mathlib source.
12
13The proof chooses a prime factor of `n! + 1`. If that prime factor were at most `n`, it would divide `n!`. Since it also divides `n! + 1`, it would divide one, contradicting primality. Thus the chosen prime is at least `n`.
14
15This argument establishes existence; it does not promise that the chosen prime is the smallest prime above `n`.
16
18
19The set of primes is not bounded above. The set of primes is infinite. The pinned mathlib version has separate declarations for these formulations, linked by proofs. They should be separate Claims connected by derivation links, not collapsed into one string-matched record.
20
21## A deliberately bounded follow-up task
22
23Formalize the strict variant: for every `n`, find a prime `p` with `n < p`. Applying the existing non-strict theorem at `n + 1` gives a short proof. This is an implementation and explanation exercise, not an unsolved mathematical problem.
24
25A tempting failed attempt applies the non-strict theorem at `n` and directly returns its witness. It only provides `n ≤ p`, which is weaker than the requested `n < p`. Keep this failure visible as an example of useful negative work and verifier feedback.
26
27## Reading the evidence
28
29A Lean success checks the submitted formal statement against a pinned environment. It does not, by itself, prove that this note's informal wording is perfectly aligned with the declaration, that this explanation is independently reviewed, or that the corpus covers all equivalent formalizations.
30