Alphabeta MathHow 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.
Example
For the Klein four group ,
Facts & Assumptions
Given: The four-element group .
( The holomorph ).
The holomorph acts faithfully on the underlying set of ( The holomorph acts faithfully on by affine permutations ).
is the group of all permutations of a four-element set (The symmetric group : the bijections of a set under composition).
A four-element set has bijections (A finite set with has exactly bijections onto itself, and bijections onto any set of the same cardinality).
Verification
Every automorphism of fixes the identity and permutes the three nonidentity elements. Conversely, any permutation of those three elements preserves the group law: the product of two distinct nonidentity elements is the third. Thus and has order six.
By [L1], . By [L2] and [L3], its faithful action embeds it into , which also has elements by [L4].
An injective map between these two finite sets of equal size is surjective. Hence the embedding is an isomorphism.
Depends on
- The holomorph $\operatorname{Hol}(G)=G\rtimes\operatorname{Aut}(G)$
- The holomorph acts faithfully on $G$ by affine permutations $x\mapsto g\alpha(x)$
- The symmetric group $\operatorname{Sym}(X)$: the bijections of a set $X$ under composition
- A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality
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: 52 results over 15 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
- Peter J. Cameron, The Holomorph of a Group (standard reference, not scraped)