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.
in both directions: the six-vertex argument and the red -cycle whose blue complement is another -cycle
Example
The equality in The Ramsey number can be read directly on labelled complete graphs. Complete graphs are those of Empty and complete graphs, complete bipartite graphs, and the convention that and have vertices, and the blue graph in the lower witness is the complement in the sense of Graph isomorphisms, automorphisms and graph complements.
Facts & Assumptions
Given: Vertices for the upper witness and for the lower witness; finite pigeonhole is If then every has a fibre with more than elements, and for nonempty some fibre has at least elements.
The Ramsey number satisfies (The Ramsey number ).
Verification
At vertex of a red-blue , three incident edges share a colour. If they are and red, then a red edge among closes a red triangle, while the absence of such an edge makes a blue triangle. Exchanging colours covers the other case.
On , colour red and the other edges blue. The red graph is the cycle ; the blue graph is the cycle . Neither cycle has a triangle. This gives a five-vertex avoidance colouring and, together with step 1.1, verifies both sides of [L1].
Depends on
- The Ramsey number $R(3,3)=6$
- If $\lvert A\rvert > k\lvert B\rvert$ then every $f : A \to B$ has a fibre with more than $k$ elements, and for nonempty $B$ some fibre has at least $\lceil \lvert A\rvert / \lvert B\rvert\rceil$ elements
- Empty and complete graphs, complete bipartite graphs, and the convention that $P_n$ and $C_n$ have $n$ vertices
- Graph isomorphisms, automorphisms and graph complements
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: 58 results over 16 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
- Douglas West, Combinatorial Game Theory, Ramsey example (standard reference, not scraped)