TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Finite graph Ramsey theorem: $\binom{s+t-2}{s-1}\to(s,t)^2$ for all positive $s,t$

Statement

For all positive natural numbers $s,t$ ,

$\binom{s+t-2}{s-1}\to(s,t)^2.$

The arrow notation is Finite colourings of $k$ -element subsets, monochromatic sets, and the arrow notations $N\to(s,t)^2$ and $N\to(r)^k_c$ , binomial coefficients are those of The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ , and the induction is over the natural order of Order on the natural numbers using The principle of mathematical induction.

Facts & Assumptions

Given: Positive natural numbers $s,t$ .

[L1]

If $m\to(s-1,t)^2$ and $n\to(s,t-1)^2$ , then $m+n\to(s,t)^2$ for $s,t\ge2$ (If $m\to(s-1,t)^2$ and $n\to(s,t-1)^2$ , then $m+n\to(s,t)^2$ for $s,t\ge2$ ).

[L2]

Pascal's rule. $\displaystyle\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}$ (Pascal's rule $\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}$ , and the hockey-stick identity $\sum_{i \le n}\binom{i}{k} = \binom{n+1}{k+1}$ ).

Proof

technique · induction

1.1

If $s=1$ or $t=1$ , every nonempty vertex set contains the required one-vertex set in the corresponding colour convention, and the displayed binomial coefficient is $1$ .

base

1.2

Assume $s,t\ge2$ and that the formula holds whenever the sum of the two positive parameters is smaller than $s+t$ . Then $\binom{s+t-3}{s-2}\to(s-1,t)^2$ and $\binom{s+t-3}{s-1}\to(s,t-1)^2$ by the induction hypothesis.

2.1

Apply [L1] to the two witnesses in step 1.2 and use [L2] to identify their sum as $\binom{s+t-2}{s-1}$ . This gives the displayed arrow for $(s,t)$ .

step 1.2L1L2

3.1

The base faces and the induction step cover all positive $s,t$ , so the explicit binomial witness works universally.

step 1.1step 2.1discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 69 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. Fox et al., Graph Ramsey Theory, Section 2.1 (standard reference, not scraped)
R. Diestel, Graph Theory, 6th ed., Theorem 9.1.1 (standard reference, not scraped)

Finite graph Ramsey theorem: (s+t−2s−1)→(s,t)2\binom{s+t-2}{s-1}\to(s,t)^2(s−1s+t−2​)→(s,t)2 for all positive s,ts,ts,t