Alphabeta Math
LemmaStatement: Literature-sourcedProof: 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.

Left identity for addition

Statement

For all n∈Nn \in \mathbb{N}: 0+n=n0 + n = n. The right identity n+0=nn + 0 = n is definitional, so together with this law 00 is a two-sided identity for addition.

Facts & Assumptions

Given: Addition with m+0=mm + 0 = m and m+σ(n)=σ(m+n)m + \sigma(n) = \sigma(m + n) (Addition of natural numbers).

[L1]

Induction principle (The principle of mathematical induction).

Proof

technique · induction
1.1

Base n=0n = 0: 0+0=00 + 0 = 0 by the clause m+0=mm + 0 = m at m=0m = 0.

base
1.2

Inductive hypothesis: 0+n=n0 + n = n.

ih
2.1

Step: 0+σ(n)=σ(0+n)=σ(n)0 + \sigma(n) = \sigma(0 + n) = \sigma(n), using m+σ(n)=σ(m+n)m + \sigma(n) = \sigma(m + n) at m=0m = 0, then the hypothesis.

step 1.2given
3.1

By induction [L1], 0+n=n0 + n = n for all n∈Nn \in \mathbb{N}.

step 1.1step 2.1discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 15 results over 9 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