openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance

Lemma · version 1

Characterizing a natural-number prime

Earlier version 1. View current version 2 →

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_def

Commit 32d24245c7a12ded17325299fd41d412022cd3fe

Connections

In this problem · publication v3 · 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.

Sources

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.

Record details
Claim ID
claim-prime-divisor-characterization
Statement version
1
SHA-256
e28a3f0a81e534dc1bfdf33247edada0eec36eb7f36624c20103aa5f5d2f04e0

Publication records