ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

Up to isomorphism the four-vertex path is the only prime graph on four vertices

Example

Up to isomorphism, the only prime graph on four vertices is the path $P_{4}$ .

Facts & Assumptions

Given: A graph $G$ on four vertices.

[L1]

Every union of connected components is a module, and every union of anticonnected components is a module (Every union of connected components is a module, and so is every union of anticonnected components).

[L2]

A prime graph has only trivial modules (Prime graphs: those whose only modules are the trivial ones, Modules of a graph, and the trivial modules).

[L3]

The path $P_{4}$ is prime (The four-vertex path has only trivial modules).

Verification

technique · direct

1.1

If $G$ is prime, then $G$ is connected and anticonnected. Indeed, if $G$ were disconnected, some union of connected components would have size $2$ or $3$ ; by [L1] that union would be a nontrivial module, contradicting [L2]. The same argument in $\overline{G}$ shows that if $\overline{G}$ were disconnected, a union of anticomponents of $G$ would be a nontrivial module.

L1L2

2.1

Let $G$ be connected and anticonnected. No vertex has degree $0$ , since $G$ is connected, and no vertex has degree $3$ , since such a vertex is isolated in $\overline{G}$ . Thus every vertex has degree $1$ or $2$ .

step 1.1given

3.1

Some vertex has degree $1$ . Otherwise every vertex has degree $2$ ; following neighbours from any vertex then forces the four vertices to form $C_{4}$ , whose complement is the disjoint union of two edges, contrary to anticonnectedness.

step 2.1given

4.1

Let $v_{0}$ have unique neighbour $v_{1}$ . Connectivity gives $v_{1}$ a neighbour $v_{2} \neq v_{0}$ , and connectivity of the remaining vertex $v_{3}$ forces an edge from $v_{3}$ to $v_{1}$ or $v_{2}$ . The edge $v_{1} v_{3}$ is impossible, since then $v_{1}$ has degree $3$ ; hence $v_{2} v_{3}$ is an edge. There are no further edges: $v_{0}$ has degree $1$ , $v_{1} v_{3}$ was excluded, and $v_{2}$ already has the two neighbours $v_{1}, v_{3}$ . Therefore $G$ is the path $v_{0} v_{1} v_{2} v_{3}$ .

step 2.1step 3.1given

5.1

Every prime graph on four vertices is therefore isomorphic to $P_{4}$ , and [L3] shows that $P_{4}$ is prime.

step 1.1step 4.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Chudnovsky, The Erdős–Hajnal Conjecture — A Survey, sec. 2 (standard reference, not scraped)