Alphabeta Math
Session-authored (Fable 5 assisted)
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.

7 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Plane Graphs, Euler's Formula and the Five Colour Theorem — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Euler's formula checked on a plane tree, a cycle, and the four-face embedding of K4K_4

Example

Euler's formula gives the same value on a plane tree, a cycle, and the tetrahedral embedding of K4K_4.

Facts & Assumptions

Given: A plane tree on n1n\ge1 vertices, a plane cycle on n3n\ge3 vertices, and the standard plane embedding of K4K_4.

[L1]

Every connected plane graph satisfies VE+F=2|V|-|E|+|F|=2 (Euler's formula VE+F=2|V|-|E|+|F|=2 for every connected plane graph).

[L2]

A finite forest satisfies V=E+c|V|=|E|+c, so a tree on nn vertices has n1n-1 edges (For every forest, V=E+c|V|=|E|+c, where cc is the number of connected components).

Verification

technique · direct
1.1

By [L2], a tree on nn vertices has n1n-1 edges, and its plane embedding has one face by Every plane forest has exactly one face. Thus VE+F=n(n1)+1=2|V|-|E|+|F|=n-(n-1)+1=2. This includes the one-vertex tree, for which the edge count is zero.

L1L2algebra
1.2

A plane cycle CnC_n, in the notation of Empty and complete graphs, complete bipartite graphs, and the convention that PnP_n and CnC_n have nn vertices, has nn vertices and nn edges. Its polygon bounds one face and has the unbounded face on the other side, so VE+F=nn+2=2|V|-|E|+|F|=n-n+2=2.

L1algebra
2.1

Embed three vertices of K4K_4 as a triangle and place the fourth inside it, joined to all three corners. The graph has four vertices, six edges, three bounded triangular faces, and the unbounded triangular face. Hence VE+F=46+4=2|V|-|E|+|F|=4-6+4=2, as [L1] requires.

L1constructalgebra
CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

K4K_4 is planar but has chromatic number four, so the five-colour bound cannot be lowered to three

Statement refuted

The conclusion of Five colour theorem: every planar graph has chromatic number at most five can be strengthened to say that every planar graph is three-colourable.

Facts & Assumptions

Counterexample

technique · direct
1.1

Draw three vertices as a triangle, place the fourth inside it, and join that vertex to the three corners. The six edges meet only at their common endpoints, so this is a plane embedding of K4K_4.

F2construct
2.1

By [F1] and [F2], the four vertices must receive pairwise distinct colours in any proper colouring. Assigning a different colour to each vertex is proper, so χ(K4)=4\chi(K_4)=4. Thus a planar graph need not be three-colourable, although Five colour theorem: every planar graph has chromatic number at most five supplies five colours for every planar graph.

F1F2step 1.1
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The Petersen graph is nonplanar by an explicit subdivision of K3,3K_{3,3} after deleting one vertex

Example

Deleting one vertex from the Petersen graph exposes a subdivision of K3,3K_{3,3}.

Facts & Assumptions

Given: Label a Petersen vertex by a two-element subset of {1,2,3,4,5}\{1,2,3,4,5\}, with adjacency exactly when labels are disjoint, as in The Petersen graph on the two-element subsets of a five-element set, adjacent when disjoint.

[L1]

A finite graph is planar exactly when it contains neither a subdivision of K5K_5 nor a subdivision of K3,3K_{3,3} (Kuratowski–Wagner theorem: a finite graph is planar exactly when it has neither a K5K_5 nor a K3,3K_{3,3} minor, equivalently neither subdivision).

[F1]

Two Petersen vertices are adjacent exactly when their two-element labels are disjoint (The Petersen graph on the two-element subsets of a five-element set, adjacent when disjoint).

Verification

technique · constructive
1.1

Delete the vertex 1212. Take the branch classes A={13,14,15}A=\{13,14,15\} and B={23,24,25}B=\{23,24,25\}. The six direct branch connections are 1313 to 24,2524,25, 1414 to 23,2523,25, and 1515 to 23,2423,24. The remaining three are the paths 13452313-45-23, 14352414-35-24, and 15342515-34-25.

F1construct
2.1

Every consecutive pair in the displayed list has disjoint labels, so it is an edge by [F1]. The internal vertices 45,35,3445,35,34 are distinct and are not branch vertices; all other listed connections are single edges. Thus the nine paths are internally disjoint and form a subdivision, in the sense of Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors, of K3,3K_{3,3} with branch classes AA and BB. This subdivision lies in a subgraph of the Petersen graph, so [L1] proves that the Petersen graph is nonplanar.

L1F1step 1.1discharge-construct
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Two plane embeddings of one connected planar graph have nonisomorphic dual multigraphs

Example

The abstract graph below has two plane embeddings whose dual multigraphs are distinguished by their degree multisets. For a finite multigraph with the endpoint map of Multigraphs, loops and directed graphs as variants distinct from the default finite simple graph, count an ordinary incident edge once and a loop twice in the degree. An isomorphism of such endpoint-map structures is a pair of vertex and edge bijections preserving endpoints, and therefore preserves the degree multiset.

Facts & Assumptions

Given: Let GG have vertices s,t,a,b,c,ws,t,a,b,c,w. Its edges form three internally disjoint ss-tt paths P1=stP_1=st, P2=satP_2=sat, and P3=sbctP_3=sbct, together with the bridge swsw.

[F1]

An endpoint-preserving multigraph isomorphism preserves the degree multiset because it bijects the incident edge-ends at every vertex, with a loop contributing two ends.

Verification

technique · constructive
1.1

Embed the three ss-tt paths in cyclic order. Write f12,f23,f31f_{12},f_{23},f_{31} for the faces between the indicated path pairs. In the dual of The plane dual multigraph, with a vertex for each face and one crossing edge for each primal edge, the path lengths 1,2,31,2,3 give respectively that many parallel dual edges between the two faces on each side of the path. Before accounting for swsw, the degrees of f12,f23,f31f_{12},f_{23},f_{31} are 3,5,43,5,4. The bridge may be drawn into any one of these face sectors at ss; it then gives a dual loop at that face.

L1construct
2.1

In one embedding draw swsw into f12f_{12}; the dual degree multiset is then {5,5,4}\{5,5,4\}. In another draw it into f31f_{31}; the dual degree multiset is {3,5,6}\{3,5,6\}. These multisets differ, since a loop contributes two to its incident degree. By [F1] the two dual multigraphs are nonisomorphic, although both arise from the same connected planar graph GG.

L1F1step 1.1discharge-construct
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

A degree-five vertex is inserted into a plane graph after one explicit Kempe-chain colour swap

Example

One Kempe swap extends a five-colouring across the centre of a plane wheel with five rim vertices.

Facts & Assumptions

Given: Let v1,v2,v3,v4,v5v_1,v_2,v_3,v_4,v_5 occur in this cyclic order on a plane 55-cycle. Colour viv_i with colour ii, and plan to insert a vertex vv inside the cycle adjacent to every viv_i.

[L1]

Swapping two colours on one Kempe component preserves a proper colouring (Swapping the two colours on one Kempe component preserves a proper colouring).

[L2]

The alternating Kempe connections between cyclic neighbours v1,v3v_1,v_3 and v2,v4v_2,v_4 cannot both occur (For five cyclically ordered neighbours of a plane vertex, alternating Kempe paths between the first and third and between the second and fourth cannot both occur).

Verification

technique · constructive
1.1

Before vv is inserted, its five prospective neighbours use all five colours. In the subgraph induced by colours 11 and 33, both v1v_1 and v3v_3 are isolated: their two cycle neighbours have colours 2,52,5 and 2,42,4, respectively. In particular there is no alternating 11-33 path between them, consistently with [L2].

L2construct
2.1

Swap colours 11 and 33 on the Kempe component {v1}\{v_1\}. The colouring remains proper by [L1]; now both v1v_1 and v3v_3 have colour 33, but they are nonadjacent, and no rim vertex has colour 11. Give the inserted centre vv colour 11. Every spoke then has differently coloured endpoints, producing an explicit five-colouring of the plane wheel and illustrating the swap used in Five colour theorem: every planar graph has chromatic number at most five.

L1step 1.1discharge-construct
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

K3,3K_{3,3} satisfies E3V6|E|\le3|V|-6 but is nonplanar, so the planar edge bound is not sufficient

Statement refuted

Every finite simple graph with n3n\ge3 vertices and at most 3n63n-6 edges is planar.

Facts & Assumptions

[L1]

Every simple planar graph with n3n\ge3 vertices has at most 3n63n-6 edges (Every simple planar graph with n3n\ge3 vertices has at most 3n63n-6 edges, with equality for every plane triangulation).

[L2]

The graph K3,3K_{3,3} is nonplanar (K5K_5 and K3,3K_{3,3} are nonplanar).

Counterexample

technique · direct
1.1

The two parts of K3,3K_{3,3} contain three vertices each, so V=6|V|=6. Every vertex in either part is adjacent to all three vertices of the other part, giving E=33=9|E|=3\cdot3=9; equivalently this follows from Handshake lemma: the sum of the vertex degrees is twice the number of edges. Consequently 9366=129\le3\cdot6-6=12, so the necessary inequality in [L1] holds.

L1algebra
2.1

Nevertheless [L2] says that this graph is nonplanar. Hence satisfying the planar simple-graph edge bound does not suffice for planarity.

L2step 1.1
CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

An injective nonpolygonal arc drawing is excluded by the page's finite polygonal plane-graph convention

Statement refuted

Every injective continuous drawing of an abstract edge is a plane graph under this page's definition.

Facts & Assumptions

Given: Let γ:[0,1]R2\gamma:[0,1]\to\mathbb R^2 be defined by γ(0)=(0,0)\gamma(0)=(0,0) and γ(t)=(t,tsin(1/t))\gamma(t)=(t,t\sin(1/t)) for t>0t>0.

[F1]

A path is a continuous map from the unit interval (Paths, path-connected spaces and path components).

[L1]

Counterexample

technique · direct
1.1

The first coordinate of γ(t)\gamma(t) is tt, so γ\gamma is injective. For t>0t>0 it is continuous, and tsin(1/t)t|t\sin(1/t)|\le t shows continuity at 00. Thus [F1] makes it a continuous arc with distinct endpoints. It is not polygonal: the second coordinate vanishes at infinitely many points t=1/(kπ)t=1/(k\pi) accumulating at 00 and changes sign between them, whereas a finite union of line segments either has only finitely many such crossings of the horizontal axis or contains a nontrivial segment of that axis. The latter is impossible here because tsin(1/t)t\sin(1/t) is not identically zero on any interval.

F1construct
2.1

Use the image of γ\gamma as the drawing of the sole edge of a two-vertex abstract graph. The drawing is injective but its edge is not a polygonal arc in the sense of Polygonal arcs and polygons as non-self-intersecting finite unions of line segments in R2\mathbb R^2, so [L1] excludes this particular drawing from the page's class of plane graphs. This does not make the abstract one-edge graph nonplanar: drawing its edge as a straight segment gives a plane embedding.

L1step 1.1construct

Sources