ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

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.

$1+1=2$ from the recursion

Example

With $1 = \sigma(0)$ and $2 = \sigma(1) = \sigma(\sigma(0))$ , the recursive definition of addition gives $1 + 1 = 2$ . This is the archetypal proof by unfolding a recursive definition.

Facts & Assumptions

Given: addition $m + 0 = m$ , $m + \sigma(n) = \sigma(m + n)$ (Addition of natural numbers); numerals $1 = \sigma(0)$ , $2 = \sigma(1)$ (The natural numbers $\mathbb{N}$ (von Neumann)).

Verification

technique · direct

1.1

By definition $1 = \sigma(0)$ and $2 = \sigma(1) = \sigma(\sigma(0))$ .

given

1.2

$1 + 0 = 1$ , by $m + 0 = m$ with $m = 1$ .

given

2.1

$1 + 1 = 1 + \sigma(0) = \sigma(1 + 0)$ , by $m + \sigma(n) = \sigma(m + n)$ with $m = 1$ , $n = 0$ .

step 1.1given

3.1

Hence $1 + 1 = \sigma(1 + 0) = \sigma(1) = 2$ .

step 2.1step 1.2∎

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: 18 results over 10 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

T. Tao, Analysis I, 3rd ed., §2.1-2.3 (Peano axioms, recursion, arithmetic) (standard reference, not scraped)
Peano axioms (Wikipedia) (standard reference, not scraped)
W. Aitken, MATH 378 Ch. 1: The Peano Axioms (CSU San Marcos) (standard reference, not scraped)

1+1=21+1=21+1=2 from the recursion