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.

Erdős's finite counting bound $R(k,k)>2^{k/2}$ for every $k\ge3$

Statement

For every natural $k\ge3$ , the diagonal Ramsey number satisfies

$R(k,k)>2^{k/2},$

where $R$ is The off-diagonal Ramsey number $R(s,t)$ as the least $N$ with $N\to(s,t)^2$ , for positive $s,t$ , real rational powers are those of Rational powers $a^r$ of a positive base and Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ , and the finite powers and products below use Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ , The product rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ and The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition.

Facts & Assumptions

Given: A natural $k\ge3$ and $N:=\lfloor2^{k/2}\rfloor$ ; binomial coefficients are as in The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ .

[L1]

If $A$ and $B$ are finite, then $A^{B}$ is finite and $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$ (The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$ ).

[L2]

If $n,k\in\mathbb N$ and $k\le n$ , then $\binom{n}{k}\cdot k!\cdot (n-k)! = n!$ , equivalently $\binom nk\,k!=n^{\underline k}$ ( $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le 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}$ ).

[L3]

Every real $x$ has a unique integer $\lfloor x\rfloor$ with $\lfloor x\rfloor\le x<\lfloor x\rfloor+1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ ).

Proof

technique · direct

1.1

There are $\binom N2$ edges in $K_N$ , and [L1] therefore counts exactly $2^{\binom N2}$ red-blue edge colourings.

2.1

For a fixed $k$ -vertex set, exactly $2\cdot2^{\binom N2-\binom k2}$ colourings make all its edges monochromatic. Summing these finite bad sets over the $\binom Nk$ choices, with overlaps allowed, shows that a colouring with no monochromatic $k$ -set exists whenever $2\binom Nk2^{-\binom k2}<1$ .

step 1.1L1

3.1

If $N<k$ , then $\binom Nk=0$ by the definition of the binomial coefficient. If $k\le N$ , [L2] gives $\binom Nk\,k!=N^{\underline k}\le N^k$ , so again $\binom Nk\le N^k/k!$ . Since $N\le2^{k/2}$ , the left side in step 2.1 is therefore at most $2^{1+k/2}/k!$ in either case. At $k=3$ this is $2^{5/2}/6<1$ ; thereafter the ratio of the bound for $k+1$ to that for $k$ is $\sqrt2/(k+1)<1$ . Hence the strict inequality holds for every $k\ge3$ .

step 2.1L2algebra

4.1

Step 2.1 supplies a colouring on $N$ vertices with no monochromatic $k$ -set, so $R(k,k)>N$ . As $R(k,k)$ is an integer and $N=\lfloor2^{k/2}\rfloor$ , [L3] implies $R(k,k)\ge N+1>2^{k/2}$ .

step 3.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 117 results over 31 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)

Erdős's finite counting bound R(k,k)>2k/2R(k,k)>2^{k/2}R(k,k)>2k/2 for every k≥3k\ge3k≥3