Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Van der Waerden's theorem, strengthened so the progression and its common difference have one colour

Statement

For all positive m,c there is a natural N such that every c-colouring of {1,…,N} contains positive integers a,d for which

a,a+d,…,a+(m−1)d,d

all have one colour. In particular, the first m displayed terms form a monochromatic arithmetic progression with positive common difference. The proof uses the focusing lemma Finite colour focussing extends equally coloured progressions to a longer monochromatic arithmetic progression and natural induction The principle of mathematical induction.

Facts & Assumptions

Given: Positive natural numbers m,c and a c-colouring of a sufficiently long positive initial interval.

[L1]

Under the length-(m−1) induction hypothesis, finite colour focussing produces either a monochromatic m-term progression or focused (m−1)-term progressions of all available colours (Finite colour focussing extends equally coloured progressions to a longer monochromatic arithmetic progression).

Proof

technique · induction
1.1baseL1

Ordinary van der Waerden existence follows by induction on m. Length 1 is immediate. Assuming finite witnesses for length m−1 for every number of colours, apply [L1] with r=c; if its first alternative occurs, it gives length m, while in the second alternative the focus has one of the c colours and extends the focused progression of that colour to length m.

2.1ihstep 1.1

We now prove the strengthened statement. If m=1, take a=d=1, so assume m≥2. Induct on c. The assertion is immediate for c=1. Assume it for c−1 colours and let n be a finite witness for the same target length m with c−1 colours. By step 1.1, choose an ordinary monochromatic progression a,a+d,…,a+n(m−1)d in a sufficiently long c-coloured interval.

3.1step 2.1ih

If one of d,2d,…,nd has the progression's colour, say td does, then a,a+td,…,a+(m−1)td together with its difference td has one colour. Otherwise the colouring t↦colour⁡(td) on {1,…,n} uses at most c−1 colours. The induction hypothesis gives u,u+q,…,u+(m−1)q,q of one colour there, and multiplication by d gives the required progression and difference in the original colouring.

4.1step 3.1discharge-induction∎

The colour induction proves the strengthened theorem for every finite c, while step 1.1 supplies the ordinary finite witnesses used in its construction.

Depends on

Used by

Dependency tree · two levels

9 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