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.

The random-colouring proof of $R (k, k) > 2^{k / 2}$

Example

For every natural $k \geq 3$ , a uniformly random red-blue colouring of the edges of a suitable complete graph proves the strict diagonal Ramsey bound $R (k, k) > 2^{k / 2} .$

Facts & Assumptions

Given: A natural $k \geq 3$ and $n = ⌊ 2^{k / 2} ⌋$ .

[L1]

A uniform red-blue edge colouring is equivalently $G (n, 1 / 2)$ (The Erdős-Rényi finite random graph $G (n, p)$ ).

[L2]

Prescribing $r$ edge colours has probability $2^{- r}$ (A prescribed set of present and absent edges in $G (n, p)$ has product probability).

[L3]

Probability of a finite union is at most the sum of its event probabilities, complements have complementary probabilities, and positive probability yields a witness (The finite union bound, Normalization, nonnegativity, monotonicity, complements, and differences in a finite probability space, An event of positive probability in a finite probability space is nonempty).

[L4]

$R (k, k)$ is the least order forcing a monochromatic $k$ -clique, and the published theorem states the same strict bound (The off-diagonal Ramsey number $R (s, t)$ as the least $N$ with $N \to (s, t)^{2}$ , for positive $s, t$ , Erdős's finite counting bound $R (k, k) > 2^{k / 2}$ for every $k \geq 3$ ).

[L5]

Binomial coefficients have the factorial formula, and $n$ is the integer part of $2^{k / 2}$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , Rational powers $a^{r}$ of a positive base, Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Verification

technique · constructive

1.1

Construct the random colouring by colouring every edge independently and uniformly red or blue. A fixed $k$ -set is monochromatic with probability $2 \cdot 2^{- (\binom{k}{2})} = 2^{1 - (\binom{k}{2})}$ .

L1L2construct

2.1

The union bound over all $k$ -sets gives failure probability at most $2 (\binom{n}{k}) 2^{- (\binom{k}{2})} \leq 2 n^{k} 2^{- (\binom{k}{2})} / k! \leq 2^{1 + k / 2} / k!$ .

step 1.1L3L5algebra

3.1

At $k = 3$ , $3! = 6 > 2^{5 / 2}$ . If $k! > 2^{1 + k / 2}$ for $k \geq 3$ , then $(k + 1)! = (k + 1) k! > 2^{1 + (k + 1) / 2}$ because $k + 1 > \sqrt{2}$ . Hence the final bound in step 2.1 is less than $1$ for every $k \geq 3$ .

step 2.1algebra

4.1

By [L3] a colouring with no monochromatic $k$ -set exists on $n$ vertices, so $R (k, k) > n$ . Since $R (k, k)$ is an integer and $n = ⌊ 2^{k / 2} ⌋$ , this implies $R (k, k) > 2^{k / 2}$ and agrees with [L4].

step 3.1L3L4L5discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

79 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

J. Matousek and J. Vondrak, The Probabilistic Method, Section 2.1 (standard reference, not scraped)

The random-colouring proof of R(k,k)>2k/2R(k,k)>2k/2