Formalizing R(3,3)=6 in Rocq

This post formalizes the theorem $R(3,3) = 6$ in Rocq (formerly Coq), using computational brute force to check all 32768 possible colorings of a 6-vertex graph in under a second.

The Friends and Strangers Theorem

In 1930, Frank Ramsey proved a general theorem in his paper “On a Problem of Formal Logic” that had a remarkable combinatorial consequence. The simplest case states:

In any group of six people, either three of them mutually know each other, or three of them are mutual strangers.

We can phrase this in graph theory. Color each edge of the complete graph $K_6$ either red (friends) or blue (strangers). The theorem says every such coloring contains a monochromatic triangle - three vertices whose connecting edges share the same color.

The complete graph K₆ has:
- 6 vertices (people)
- 15 edges (pairs of people)
- 20 triangles (triples of people)

Any 2-coloring of its edges contains a monochromatic triangle.

The number 6 is tight. There exists a 2-coloring of $K_5$ with no monochromatic triangle - draw a pentagon with its vertices connected by red edges and its diagonals by blue edges. Neither the red nor blue edges form a triangle.

This is a special case of Ramsey’s theorem. The Ramsey number $R(r, s)$ is the smallest $n$ such that every 2-coloring of $K_n$ contains either a red $K_r$ or a blue $K_s$ . Our theorem says $R(3,3) = 6$ : six vertices guarantee a monochromatic triangle, and five don’t.

The Classical Proof

The textbook proof uses the pigeonhole principle. Pick any vertex $v$ in $K_6$ . It has 5 edges to the other vertices. By pigeonhole, at least 3 of these edges share a color - say red.

Let these three neighbors be $a$ , $b$ , $c$ . Now examine the triangle $\{a, b, c\}$ :

If any edge among $a$ , $b$ , $c$ is red, that edge plus $v$ forms a red triangle
If all edges among $a$ , $b$ , $c$ are blue, we have a blue triangle

Either way, a monochromatic triangle exists.

The proof is elegant, but it still rests on our own reasoning, definitions, and correct application of pigeonhole. A proof assistant mechanically verifies every logical step, removing that dependence on informal trust.

The Computational Approach

For a theorem about small finite structures, we can use brute force: enumerate every possible case and check them all.

$K_6$ has 15 edges. Each edge has 2 possible colors. That’s $2^{15} = 32768$ colorings. $K_6$ has 20 triangles. For each coloring, we check if any triangle is monochromatic.

The strategy:

Represent colorings as length-15 bitvectors
Define a boolean function has_mono_triangle that checks all 20 triangles
Enumerate all $2^{15}$ bitvectors
Prove computationally that has_mono_triangle returns true for all of them

Rocq can execute this enumeration at compile time using vm_compute (a bytecode-compiled reduction tactic), verifying the theorem by running the checker.

Setting Up the Rocq Development

Rocq is the first version under the new name (formerly Coq). We use only the standard library.

From Coq Require Import List Bool Arith.
Import ListNotations.

Edge and Triangle Indices

Rather than build a graph theory library, we hardcode the structure. $K_6$ vertices are $\{0, 1, 2, 3, 4, 5\}$ . Edges are pairs $(i, j)$ with $i < j$ , indexed 0 through 14:

(* K₆ edges in lexicographic order *)
(* 0:(0,1)  1:(0,2)  2:(0,3)  3:(0,4)  4:(0,5)  *)
(* 5:(1,2)  6:(1,3)  7:(1,4)  8:(1,5)           *)
(* 9:(2,3)  10:(2,4) 11:(2,5)                   *)
(* 12:(3,4) 13:(3,5)                            *)
(* 14:(4,5)                                     *)

Each triangle is identified by three edge indices. The 20 triangles of $K_6$ :

Definition triangles6 : list (nat * nat * nat) :=
  [ (0,1,5); (0,2,6); (0,3,7); (0,4,8);
    (1,2,9); (1,3,10); (1,4,11);
    (2,3,12); (2,4,13); (3,4,14);
    (5,6,9); (5,7,10); (5,8,11);
    (6,7,12); (6,8,13); (7,8,14);
    (9,10,12); (9,11,13); (10,11,14);
    (12,13,14) ].

The Boolean Checker

A coloring is a list bool of length 15, with edge colors looked up by index:

Definition edge_color (bits : list bool) (i : nat) : bool :=
  nth i bits false.

A triangle $(e_1, e_2, e_3)$ is monochromatic if all three edges have the same color:

Definition is_mono (bits : list bool) (tri : nat * nat * nat) : bool :=
  let '(e1, e2, e3) := tri in
  let c1 := edge_color bits e1 in
  let c2 := edge_color bits e2 in
  let c3 := edge_color bits e3 in
  Bool.eqb c1 c2 && Bool.eqb c2 c3.

The main checker tests whether any triangle is monochromatic:

Definition has_mono_triangle6 (bits : list bool) : bool :=
  existsb (is_mono bits) triangles6.

Enumerating All Bitvectors

We generate all boolean lists of length $n$ recursively:

Fixpoint all_bool_lists (n : nat) : list (list bool) :=
  match n with
  | 0 => [ [] ]
  | S n' => map (cons false) (all_bool_lists n') ++
            map (cons true)  (all_bool_lists n')
  end.

This produces $2^n$ lists. We need to prove that any list of length $n$ appears in all_bool_lists n. The induction is routine:

Lemma in_all_bool_lists : forall n bits,
  length bits = n -> In bits (all_bool_lists n).
Proof.
  induction n; intros bits Hlen.
  - destruct bits; simpl in *; [left; auto | discriminate].
  - destruct bits as [| b bits']; simpl in *; [discriminate |].
    injection Hlen as Hlen'.
    apply in_or_app.
    destruct b.
    + right. apply in_map. apply IHn. exact Hlen'.
    + left. apply in_map. apply IHn. exact Hlen'.
Qed.

The Computational Proof

For every length-15 bitvector, we now prove that has_mono_triangle6 returns true.

Lemma all_K6_have_mono_aux :
  forallb has_mono_triangle6 (all_bool_lists 15) = true.
Proof.
  vm_compute. reflexivity.
Qed.

The vm_compute tactic compiles the term to bytecode and executes it. Rocq checks all 32768 colorings in under a second, confirming each has a monochromatic triangle.

We lift this to a universal statement:

Theorem all_K6_have_mono_triangle : forall bits,
  length bits = 15 -> has_mono_triangle6 bits = true.
Proof.
  intros bits Hlen.
  apply (proj1 (forallb_forall has_mono_triangle6 (all_bool_lists 15))).
  - exact all_K6_have_mono_aux.
  - apply in_all_bool_lists. exact Hlen.
Qed.

The forallb_forall lemma bridges boolean computation and logical quantification.

The $K_5$ Counterexample

To prove $R(3,3) = 6$ rather than just $R(3,3) \leq 6$ , we exhibit a coloring of $K_5$ with no monochromatic triangle.

The classic construction: draw a pentagon and its inscribed star. Color the pentagon edges (0-1, 1-2, 2-3, 3-4, 4-0) red and the star diagonals (0-2, 0-3, 1-3, 1-4, 2-4) blue.

In our edge indexing for $K_5$ (10 edges, indices 0-9):

Definition triangles5 : list (nat * nat * nat) :=
  [ (0,1,4); (0,2,5); (0,3,6);
    (1,2,7); (1,3,8); (2,3,9);
    (4,5,7); (4,6,8); (5,6,9); (7,8,9) ].

Definition has_mono_triangle5 (bits : list bool) : bool :=
  existsb (is_mono bits) triangles5.

The pentagon/star coloring as a bitvector:

(* Edges: 0:(0,1) 1:(0,2) 2:(0,3) 3:(0,4) 4:(1,2) 5:(1,3) 6:(1,4) 7:(2,3) 8:(2,4) 9:(3,4) *)
(* Pentagon (red=true): 0-1, 1-2, 2-3, 3-4, 4-0 = indices 0, 4, 7, 9, 3 *)
Definition k5_counterexample : list bool :=
  [true; false; false; true; true; false; false; true; false; true].

And the computational verification:

Lemma k5_no_mono_triangle :
  has_mono_triangle5 k5_counterexample = false.
Proof.
  vm_compute. reflexivity.
Qed.

The Complete Theorem

Combining both parts:

Theorem ramsey_3_3_is_6 :
  (* K₅ has a coloring with no monochromatic triangle *)
  (exists bits5, length bits5 = 10 /\ has_mono_triangle5 bits5 = false)
  /\
  (* Every coloring of K₆ has a monochromatic triangle *)
  (forall bits6, length bits6 = 15 -> has_mono_triangle6 bits6 = true).
Proof.
  split.
  - exists k5_counterexample. split.
    + vm_compute. reflexivity.
    + exact k5_no_mono_triangle.
  - exact all_K6_have_mono_triangle.
Qed.

Why Computational Reflection Works

Proving theorems by running computations is called proof by reflection. It works because Rocq’s type theory treats computation as a form of proof.

The core principle: if f x = true can be verified by reduction (computation), then Rocq accepts reflexivity as a proof of f x = true. The vm_compute tactic uses a bytecode virtual machine to perform this reduction efficiently.

	Traditional proof	Proof by reflection
Method	Build proof term	Run boolean checker
Proof term size	O(cases)	O(1)
Best for	General theorems	Decidable finite props

A traditional proof would require a proof term proportional to all 32768 cases. Reflection produces a minimal proof term - just reflexivity - while verification occurs during type checking.

This technique scales well. The Four Color Theorem was verified in Coq using a similar approach: reduce the infinite problem to finitely many cases, then check each computationally.

Comparison of Approaches

Approach	Proof Size	Human Insight	Machine Verification
Pigeonhole (textbook)	~10 lines	High	None
Brute force (Rocq)	~80 lines	Low	Complete
Pigeonhole (formalized)	~200+ lines	High	Complete

The brute force approach trades mathematical elegance for mechanical certainty. We didn’t need to formalize pigeonhole, subsets, or cardinality arguments. We just enumerated and checked.

This approach works well for small Ramsey numbers. For larger numbers like $R(5,5)$ (unknown, bounded between 43 and 48), the combinatorial explosion makes brute force infeasible and clever mathematics essential.

Conclusion

$R(3,3) = 6$ formalizes cleanly in Rocq 9.0 with nothing beyond the standard library. Brute force handles all $2^{15}$ cases in under a second, and reflection keeps the proof term small by shifting the work to the bytecode reducer at type-checking time. The formalization also pays a smaller tax that is worth naming: we had to commit to a specific edge ordering, a precise definition of “monochromatic,” and a proof that our enumeration is complete - the kind of precision that informal pigeonhole proofs elide. The same shape of argument scales to any decidable property of small finite structures, which is why it shows up in much larger formalizations like the Four Color Theorem.

References

Ramsey, F. P. (1930). On a Problem of Formal Logic. Proceedings of the London Mathematical Society.
Gonthier, G. (2008). Formal Proof - The Four Color Theorem. Notices of the AMS.
Narváez, D. E., Song, C., & Zhang, N. (2024). Formalizing Finite Ramsey Theory in Lean 4. CICM 2024.