Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)>2k/2

Example

For every natural k3, a uniformly random red-blue colouring of the edges of a suitable complete graph proves the strict diagonal Ramsey bound R(k,k)>2k/2.

Facts & Assumptions

Given: A natural k3 and n=2k/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 2r (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(s,t)2, for positive s,t, Erdős's finite counting bound R(k,k)>2k/2 for every k3).

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 22(k2)=21(k2).

L1L2construct
2.1

The union bound over all k-sets gives failure probability at most 2(nk)2(k2)2nk2(k2)/k!21+k/2/k!.

step 1.1L3L5algebra
3.1

At k=3, 3!=6>25/2. If k!>21+k/2 for k3, then (k+1)!=(k+1)k!>21+(k+1)/2 because k+1>2. Hence the final bound in step 2.1 is less than 1 for every k3.

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=2k/2, this implies R(k,k)>2k/2 and agrees with [L4].

step 3.1L3L4L5discharge-construct

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: 135 results over 30 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