ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

$\langle a,b\mid a^2,\ b^2,\ aba^{-1}b^{-1}\rangle\cong(\mathbb Z/2)\times(\mathbb Z/2)$

Example

The Klein four-group has the presentation

$\langle a,b\mid a^2,\ b^2,\ aba^{-1}b^{-1}\rangle\cong(\mathbb Z/2)\times(\mathbb Z/2),$

where $a$ and $b$ correspond to $(1,0)$ and $(0,1)$ .

Facts & Assumptions

Given: The presentation $P=\langle a,b\mid a^2,b^2,aba^{-1}b^{-1}\rangle$ and the direct-product group $(\mathbb Z/2)\times(\mathbb Z/2)$ .

[L1]

A map of generators that sends every relator to the identity extends uniquely to a homomorphism from the presented group (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

[L2]

Every residue class modulo $2$ has exactly one representative in $\{0,1\}$ (For $n\ge 1$ , every class in $\mathbb{Z}/n$ has one representative $r$ with $0\le r<n$ , so $\lvert\mathbb{Z}/n\rvert=n$ ; while $\mathbb{Z}/0$ is in bijection with $\mathbb{Z}$ ).

Verification

technique · constructive

1.1

Sending $a$ to $(1,0)$ and $b$ to $(0,1)$ kills the two square relators and the commutator in the abelian direct product, so [L1] constructs a homomorphism $\pi:P\to(\mathbb Z/2)\times(\mathbb Z/2)$ .

L1construct

1.2

The commutator relation gives $ab=ba$ , and the square relations reduce both exponents modulo $2$ , so every element of $P$ has one of the forms $e,a,b,ab$ .

given

2.1

Their images are $(0,0),(1,0),(0,1),(1,1)$ , which are distinct and exhaustive by [L2]; together with step 1.2, this makes $\pi$ bijective.

L2step 1.1step 1.2

3.1

Hence $P$ is isomorphic to $(\mathbb Z/2)\times(\mathbb Z/2)$ , the Klein four-group.

step 2.1discharge-construct∎

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: 80 results over 20 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

P. J. Cameron, Group Theory revision notes (standard reference, not scraped)
J. Aspnes, Group Theory (standard reference, not scraped)

⟨a,b∣a2, b2, aba−1b−1⟩≅(Z/2)×(Z/2)\langle a,b\mid a^2,\ b^2,\ aba^{-1}b^{-1}\rangle\cong(\mathbb Z/2)\times(\mathbb Z/2)⟨a,b∣a2, b2, aba−1b−1⟩≅(Z/2)×(Z/2)