ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-13

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.

A Turán-partition colouring witnesses $R (4, 3) \geq 7$

Example

Partition the six vertices of $K_{6}$ into three pairs. Colour edges inside pairs blue and edges between pairs red. This colouring has no red $K_{4}$ and no blue $K_{3}$ , so $R (4, 3) \geq 7$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

$N \to (s, t)^{2}$ means every red-blue colouring of the pairs of an $N$ -element set has a red $s$ -set or a blue $t$ -set (Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N \to (s, t)^{2}$ and $N \to (r)_{c}^{k}$ ).

[F2]

For $s, t \geq 2$ , $R (s, t) \geq (s - 1) (t - 1) + 1$ (Turán graphs give the Ramsey lower bound $R (s, t) \geq (s - 1) (t - 1) + 1$ ).

Verification

technique · bound clique sizes in each colour

1.1

A red clique contains at most one vertex from each of the three pairs, so it has size at most $3$ . A blue clique lies within a single pair, so it has size at most $2$ .

givenF1

2.1

Thus $K_{6}$ does not arrow $(K_{4}, K_{3})$ , and the Ramsey definition gives $R (4, 3) > 6$ , hence $R (4, 3) \geq 7$ .

step 1.1givenF1F2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Yufei Zhao, Graph Theory and Additive Combinatorics (standard reference, not scraped)

A Turán-partition colouring witnesses R(4,3)≥7R(4,3)≥7