ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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 \mid n$ (Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ 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 \mid a$ and $a \ne 0$ then $d \ne 0$ and $|d| \le |a|$ (If $d \mid a$ and $a \ne 0$ then $d \ne 0$ and $|d| \le |a|$ ; hence the set of divisors of a nonzero integer is bounded above by $|a|$ ).

[L3]

$|x| = x$ when $x \ge 0$ (The absolute value $|a|$ of an integer, Absolute value in $\mathbb{Z}$ : $|a| \ge 0$ ; $|a| = 0$ exactly when $a = 0$ ; $|-a| = |a|$ ; $|ab| = |a|\,|b|$ ; $-|a| \le a \le |a|$ ; and $|a| \le c$ exactly when $-c \le a \le c$ ).

[L4]

Divisibility is reflexive; $d \mid u$ means $u = dc$ for some $c$ (Divisibility is reflexive and transitive on $\mathbb{Z}$ , and is linear: if $d \mid a$ and $d \mid b$ then $d \mid ax + by$ for all integers $x, y$ ; also $d \mid a$ implies $d \mid ac$ , $-d \mid a$ and $d \mid -a$ , Divisibility in $\mathbb{Z}$ : $d \mid a$ when $a = dq$ for some integer $q$ ).

[L5]

The order on $\mathbb{Z}$ is total, antisymmetric and transitive and is compatible with addition (The integers form a totally ordered ring, Order on the integers); $\mathbb{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]

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

[L7]

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

Verification

technique · direct

1.1

$0 < 1$ : $1 = \iota(1)$ is nonnegative and differs from $0 = \iota(0)$ by injectivity of $\iota$ . 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 = \iota(j)$ with $j \ne 0$ , so $1 = \sigma(0) \le j$ and hence $1 \le x$ , because $\iota$ preserves the order.

L6L7

2.1

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

step 1.1step 1.2L2L3L5

2.2

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

step 1.1L5

3.1

The only integers $d$ with $1 \le d \le 2$ are $1$ and $2$ : if $d \ne 1$ then $1 < d$ , so $1 + 1 \le d$ by step 1.2 applied to $d - 1 > 0$ , that is $2 \le d$ , and with $d \le 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 \le 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 $\mathbb{Z}$ : $d \mid a$ when $a = dq$ 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 $\mathbb{Z}$ : for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le 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 $\mathbb{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 \mid ab$ then $p \mid a$ or $p \mid 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 65 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)

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