Proved
Proved characterization Nat.prime_def ↗
The cited source item and version only; this is not an independent OpenMath assessment.
mathlib · natural-number prime definitions · Mathlib/Data/Nat/Prime/Defs.lean lines 97–105 →
Observed Oct 1, 2026
Lemma · version 2
Characterizing a natural-number prime
Statement
A natural number p is prime exactly when p ≥ 2 and every natural-number divisor m of p is either 1 or p.
Assumptions
- Natural numbers
- Ordinary primality
Scope
Natural-number divisibility and ordinary primality.
Evidence
Source reports
Formal proofs
Pinned prime-divisor characterization ↗
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
Declaration & revision
Nat.prime_defCommit 32d24245c7a12ded17325299fd41d412022cd3fe
Connections
In this problem · publication v5 · Selected context
Why are there infinitely many primes? →
Supporting result · Proved
This prerequisite supplies the divisibility contradiction in the factorial-plus-one proof. It is a supporting theorem, not another prime-infinitude Problem.
Relationship not independently reviewed. This concerns its use in this problem.
Formalize a prime strictly above every bound → · Related problem work; no execution evidence for this statement is asserted.
In this problem · publication v8
Why are there infinitely many primes? →
Supporting result · Proved
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.
Relationship not independently reviewed. This concerns its use in this problem.
Formalize a prime strictly above every bound → · Related problem work; no execution evidence for this statement is asserted.
Sources
mathlib · natural-number prime definitions →
- Mathlib/Data/Nat/Prime/Defs.lean lines 97–105 → · Original passage ↗
Recorded wording
Is a natural number p prime exactly when p ≥ 2 and every natural-number divisor m of p is either 1 or p?
paraphrase · Licensed source links and exact source spans; attribution retained.
mathlib contributors · Revision 32d24245c7a12ded17325299fd41d412022cd3fe
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Proved characterization Nat.prime_def ↗
The cited source item and version only; this is not an independent OpenMath assessment.
Observed Oct 1, 2026 · Source passage →
Record details
- Claim ID
- claim-prime-divisor-characterization
- Statement version
- 2
- SHA-256
- bd4f39e85cd593f0bd3bb9ecf101d166b8f0ba8eb5f8db38cd7b8c4d53fd8639