ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

$2$ is prime, and it is the only even prime: every even integer $n > 2$ is composite

Example

Call an integer even when $2 ∣ n$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ), where $2 : = 1 + 1$ . Then:

$2$ is prime (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ );
every even integer $n > 2$ is composite.

So $2$ is the only even prime, and every other prime is odd.

Facts & Assumptions

Given: The integer $2 : = 1 + 1$ .

[L1]

$p$ is prime when $p > 1$ and every positive divisor of $p$ is $1$ or $p$ ; an integer $n > 1$ that is not prime is composite (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L2]

If $d ∣ a$ and $a \neq 0$ then $d \neq 0$ and $∣ d ∣ \leq ∣ a ∣$ (If $d ∣ a$ and $a \neq 0$ then $d \neq 0$ and $∣ d ∣ \leq ∣ a ∣$ ; hence the set of divisors of a nonzero integer is bounded above by $∣ a ∣$ ).

[L3]

$∣ x ∣ = x$ when $x \geq 0$ (The absolute value $∣ a ∣$ of an integer, Absolute value in $Z$ : $∣ a ∣ \geq 0$ ; $∣ a ∣ = 0$ exactly when $a = 0$ ; $∣ - a ∣ = ∣ a ∣$ ; $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; $- ∣ a ∣ \leq a \leq ∣ a ∣$ ; and $∣ a ∣ \leq c$ exactly when $- c \leq a \leq c$ ).

[L4]

Divisibility is reflexive; $d ∣ u$ means $u = d c$ for some $c$ (Divisibility is reflexive and transitive on $Z$ , and is linear: if $d ∣ a$ and $d ∣ b$ then $d ∣ a x + b y$ for all integers $x, y$ ; also $d ∣ a$ implies $d ∣ a c$ , $- d ∣ a$ and $d ∣ - a$ , Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L5]

The order on $Z$ is total, antisymmetric and transitive and is compatible with addition (The integers form a totally ordered ring, Order on the integers); $Z$ is a commutative ring (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L6]

$ι : N \to Z$ is injective, preserves addition and order, and has as image exactly the nonnegative integers, with $ι (0) = 0$ and $ι (1) = 1$ (The naturals embed in the integers).

[L7]

On $N$ : $m < k$ exactly when $σ (m) \leq k$ (Discreteness: $σ (n)$ is the immediate successor); $1 = σ (0)$ (The natural numbers $N$ (von Neumann)); $0 \leq k$ for every $k$ (Order on the natural numbers).

Verification

technique · direct

1.1

$0 < 1$ : $1 = ι (1)$ is nonnegative and differs from $0 = ι (0)$ by injectivity of $ι$ . Adding $1$ gives $1 < 1 + 1 = 2$ , so $2 > 1 > 0$ .

L5L6

1.2

There is no integer strictly between $0$ and $1$ : if $0 < x$ then $x = ι (j)$ with $j \neq 0$ , so $1 = σ (0) \leq j$ and hence $1 \leq x$ , because $ι$ preserves the order.

L6L7

2.1

Claim 1. Let $d$ be a positive divisor of $2$ . Since $2 \neq 0$ , [L2] gives $∣ d ∣ \leq ∣ 2 ∣ = 2$ , and $d > 0$ gives $∣ d ∣ = d$ , so $1 \leq d \leq 2$ by step 1.2.

step 1.1step 1.2L2L3L5

2.2

Claim 2. Let $n > 2$ with $2 ∣ n$ . Then $n > 2 > 1$ , so $n > 1$ ; and $2$ is a positive divisor of $n$ with $2 \neq 1$ (by step 1.1) and $2 \neq n$ (since $n > 2$ ).

step 1.1L5

3.1

The only integers $d$ with $1 \leq d \leq 2$ are $1$ and $2$ : if $d \neq 1$ then $1 < d$ , so $1 + 1 \leq d$ by step 1.2 applied to $d - 1 > 0$ , that is $2 \leq d$ , and with $d \leq 2$ antisymmetry gives $d = 2$ . Both $1$ and $2$ do divide $2$ . Hence the only positive divisors of $2$ are $1$ and $2$ , and $2 > 1$ , so $2$ is prime.

step 1.1step 1.2step 2.1L1L4L5

3.2

So $n$ has a positive divisor other than $1$ and $n$ , hence is not prime; being greater than $1$ , it is composite.

step 2.2L1

4.1

Claims 1 and 2 are established, and together they say $2$ is the only even prime: an even prime $n$ satisfies $n > 1$ , hence $2 \leq n$ by step 3.1's argument, and $n > 2$ is excluded because such an $n$ is composite by step 3.2; so $n = 2$ .

step 1.2step 3.1step 3.2L1L5∎

Remarks

"Even" is defined here as divisibility by $2$ , not by a new notion of parity. That is Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ applied at $d = 2$ , so no second vocabulary is introduced, and the odd integers are exactly those with remainder $1$ under Division with remainder in $Z$ : for $a \in Z$ and $b > 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < b$ .
This is why parity sufficed for the $2$ -adic case elsewhere in the library. The published The $2$ -adic absolute value gives an ultrametric on $Q$ , in which every triangle is isosceles and every point of a ball is a centre ↗ builds the $2$ -adic valuation from parity alone and records that the general $p$ -adic valuation needs primality and unique factorisation. At $p = 2$ "not divisible by $2$ " is a single condition that the division algorithm decides; for a general prime $p$ the corresponding step is Euclid's lemma: if $p$ is prime and $p ∣ a b$ then $p ∣ a$ or $p ∣ b$ .
The smallest prime is $2$ , and there is no smaller one to miss. $1$ and $0$ are excluded by the clause $p > 1$ of Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ , and negative integers by the same clause, so the classification here is complete rather than a convention about where to start.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Prime number (Wikipedia) (standard reference, not scraped)
Parity (mathematics) (Wikipedia) (standard reference, not scraped)
Old Dominion University: Two is the only even prime (standard reference, not scraped)

22 is prime, and it is the only even prime: every even integer n>2n>2 is composite