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

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.

$W (3, 2) = 9$ by an explicit colouring of ${0, \dots, 7}$ and an exhaustive symmetry-reduced proof for ${0, \dots, 8}$

Example

With the zero-based natural-number convention of The natural numbers $N$ (von Neumann) and Order on the natural numbers, the van der Waerden number of The van der Waerden number $W (k, c)$ as the least interval length forcing a monochromatic $k$ -term arithmetic progression is $W (3, 2) = 9$ . Translation identifies the intervals ${0, \dots, N - 1}$ and ${1, \dots, N}$ , so this is the same convention used by Van der Waerden's theorem, strengthened so the progression and its common difference have one colour.

Facts & Assumptions

Given: Two colours, red and blue, and three-term progressions $a, a + d, a + 2 d$ with $d > 0$ .

[L1]

Every finite colouring of a sufficiently long initial interval has a monochromatic arithmetic progression whose common difference has the same colour (Van der Waerden's theorem, strengthened so the progression and its common difference have one colour).

Verification

technique · direct

1.1

On ${0, \dots, 7}$ colour $0, 1, 4, 5$ blue and $2, 3, 6, 7$ red. Checking the possible differences $d = 1, 2, 3$ shows that every three-term progression meets both two-point colour blocks. Thus $W (3, 2) > 8$ .

construct

1.2

Suppose ${0, \dots, 8}$ has an avoiding colouring. Exchange colour names to make $4$ red. The progression $0, 4, 8$ has a blue endpoint; reflect the interval if necessary to make $0$ blue. If $2$ is red, the progressions $2, 3, 4$ and $2, 4, 6$ force $3, 6$ blue, making $0, 3, 6$ blue, a contradiction. Hence $2$ is blue, and $0, 1, 2$ forces $1$ red.

2.1

If $3$ is red, then $1, 3, 5$ forces $5$ blue, $1, 4, 7$ forces $7$ blue, $2, 5, 8$ forces $8$ red, and $4, 6, 8$ forces $6$ blue; now $5, 6, 7$ is blue. If $3$ is blue, then $0, 3, 6$ forces $6$ red, $1, 4, 7$ forces $7$ blue, and $3, 5, 7$ forces $5$ red; now $4, 5, 6$ is red. Both cases contradict avoidance, so every colouring of nine consecutive integers has a monochromatic three-term progression.

step 1.2

3.1

Steps 1.1 and 2.1 give the lower and upper bounds, hence $W (3, 2) = 9$ .

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

MIT OpenCourseWare 18.310, Chapter 3 (standard reference, not scraped)

W(3,2)=9W(3,2)=9 by an explicit colouring of {0,…,7}{0,…,7} and an exhaustive symmetry-reduced proof for {0,…,8}{0,…,8}