arxiv: 2604.21376 · v1 · submitted 2026-04-23 · 💻 cs.DM

Recognition: unknown

A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect

Jean-Philippe Chancelier (CERMICS)

Authors on Pith no claims yet

Pith reviewed 2026-05-08 13:02 UTC · model grok-4.3

classification 💻 cs.DM

keywords Sands-Sauer-Woodrow theoremformal proofRocqbinary relationsdirected graphsmonochromatic pathsindependent setstransitive closure

0 comments

The pith

Formal verification in Rocq proves a stronger form of the Sands-Sauer-Woodrow theorem on two-colored directed graphs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper delivers a machine-checked proof of the Sands-Sauer-Woodrow theorem using the Rocq assistant and the MathComp/ssreflect library. In a directed graph whose blue and red edges are given by two binary relations, the theorem guarantees an independent set S such that every vertex outside S can reach S along a monochromatic path, provided there is no monochromatic infinite outward path. The authors strengthen the hypothesis by requiring only that the asymmetric parts of the transitive closures of the two relations contain no infinite outward paths, then recover the classical statement as a corollary through a lemma that any infinite path in the asymmetric transitive closure yields an infinite path in the original relation.

Core claim

In a directed graph with blue edges Eb and red edges Er, if the asymmetric part of the transitive closure of Eb has no infinite outward path and the asymmetric part of the transitive closure of Er likewise has none, then there exists an independent set S such that every vertex not in S reaches S by a monochromatic path; this statement is proved in Rocq and the original Sands-Sauer-Woodrow theorem follows from it.

What carries the argument

The asymmetric part of the transitive closure of a binary relation, which extracts the strict reachability without reciprocal pairs and serves as the precise carrier of the infinite-path prohibition.

If this is right

The classical Sands-Sauer-Woodrow theorem is obtained immediately as a corollary.
The dedicated library of binary relations as classical sets becomes available for formalizing other infinite-graph results.
Any future proof that weakens the path condition further can be compared directly against this formal baseline.
The proof script supplies a mechanically verified template for similar reachability arguments in order-theoretic settings.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same weakening strategy may apply to other theorems that currently assume absence of infinite paths in the original relation rather than in its strict transitive closure.
Because the proof is machine-checked, it can serve as a verified component inside automated tools for graph coloring or order-extension problems.
The result suggests that many classical infinite-graph theorems rest on assumptions stronger than necessary once transitive closures are taken into account.

Load-bearing premise

The library definitions of binary relations, transitive closures, asymmetric parts, infinite outward paths, and independent sets correctly capture the informal notions in the theorem.

What would settle it

An explicit finite or countably infinite two-colored digraph in which the asymmetric transitive closures have no infinite outward paths yet no independent set S satisfies the monochromatic reachability condition would refute the claim.

read the original abstract

We present a formal proof of the Sands-Sauer-Woodrow (SSW) theorem using the Rocq proof assistant and the MathComp/SSReflect library. The SSW theorem states that in a directed graph whose edges are colored with two colors and that contains no monochromatic infinite outward path, there exists an independent set S of vertices such that every vertex outside S can reach S by a monochromatic path. We formalize the graph using two binary relations Eb and Er , representing the blue and red edges respectively, and we develop a dedicated library for binary relations represented as classical sets. Beyond formalizing the original SSW theorem, we establish a strictly stronger version in which the assumption ''no monochromatic infinite outward path'' is replaced by the weaker condition that the asymmetric parts of the transitive closures of Eb and Er admit no infinite outward paths. The original SSW theorem is then recovered as a corollary via a lemma showing that an infinite path for the asymmetric part of the transitive closure of a relation implies an infinite path for the relation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Clean Rocq formalization of the SSW theorem plus a genuine strengthening that weakens the infinite-path hypothesis.

read the letter

The main takeaway is a machine-checked Rocq proof of the Sands-Sauer-Woodrow theorem on two-edge-colored digraphs, together with a strictly stronger version. The authors replace the usual no-monochromatic-infinite-outward-path assumption with the weaker condition that the asymmetric parts of the transitive closures of the blue and red relations have no infinite outward paths, then recover the original statement via an explicit lemma showing that an asymmetric infinite path implies a full infinite path. They encode the graph as two binary relations Eb and Er, build supporting definitions for paths, closures, and independent sets inside the MathComp/ssreflect library for classical sets and relations, and carry out the entire argument from those primitives. The development stays internal to the prover with no external assumptions or fitted parameters. This approach is reliable and the strengthening is new relative to the cited literature. The formalization is self-contained and the connecting lemma is stated clearly, which makes the improvement usable for other work. The only soft spots are minor. The paper gives limited explicit discussion of how the formal notions of monochromatic reachability and independent sets line up with the original informal statement, though the structure suggests the mapping is standard. It also says little about how the new relation library might be reused on other theorems. Neither point affects the core correctness. The citation pattern is appropriate since it rests on library components rather than circular self-reference. This paper is for people working in formal verification of combinatorial statements or those who need verified graph-theoretic lemmas. A reader who wants to see a complete, machine-checked treatment of path and closure conditions in ssreflect will find it directly useful. It deserves peer review because the proof is complete, the strengthening adds value, and the formal evidence is strong.

Referee Report

0 major / 2 minor

Summary. The paper presents a formal proof in Rocq using the MathComp/ssreflect library of the Sands-Sauer-Woodrow theorem: in a directed graph with blue and red edges (formalized as binary relations Eb and Er) containing no monochromatic infinite outward path, there exists an independent set S such that every vertex outside S reaches S via a monochromatic path. It also proves a strictly stronger version replacing the hypothesis with the condition that the asymmetric parts of the transitive closures of Eb and Er have no infinite outward paths, and recovers the original theorem as a corollary via a lemma relating infinite paths in asymmetric transitive closures to those in the original relations. A dedicated library for binary relations as classical sets is developed.

Significance. If the formalization is faithful, this supplies a machine-checked proof of a graph-theoretic result from basic library definitions of relations, paths, and closures, which is a clear strength for verification and eliminates the possibility of subtle errors in the combinatorial reasoning. The stronger theorem and the explicit recovery lemma are valuable additions. Such formal developments in mature provers like Rocq with ssreflect enhance the reliability of results in discrete mathematics.

minor comments (2)

The manuscript should include an explicit discussion or table mapping the informal notions (monochromatic paths, independent sets, outward paths) to the chosen formal definitions of Eb, Er, transitive closures, and asymmetric parts to make the correspondence fully transparent to readers.
Consider adding a brief informal proof sketch of the key steps (especially the stronger version and the recovery lemma) before the formal Rocq code to improve readability for non-specialists in proof assistants.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our work, recognition of the significance of the machine-checked proof, and recommendation to accept the manuscript. No major comments were raised in the report.

Circularity Check

0 steps flagged

No circularity: machine-checked formalization from library primitives

full rationale

The paper supplies a Rocq/MathComp formalization of the SSW theorem together with a strictly stronger variant. The derivation begins from the library's standard definitions of binary relations (as classical sets), paths, independent sets, and transitive closures. The stronger statement is proved directly; the original SSW theorem is recovered by an explicit, separately stated lemma that an infinite path in the asymmetric part of the transitive closure implies an infinite path in the relation itself. All steps are internally verified by the prover; no parameters are fitted, no self-citations serve as load-bearing premises, and no equation or definition reduces to its own input by construction. The development is therefore self-contained against the external benchmark of the Rocq kernel.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on standard mathematical axioms and library lemmas for binary relations and paths; no free parameters or invented entities are introduced.

axioms (1)

standard math Standard properties of binary relations, transitive closures, asymmetric parts, and infinite paths as defined in the MathComp/ssreflect library.
The formalization builds directly on the library's established definitions for relations represented as classical sets.

pith-pipeline@v0.9.0 · 5485 in / 1333 out tokens · 85480 ms · 2026-05-08T13:02:49.241826+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

17 extracted references

[1]

Affeldt, Y

R. Affeldt, Y. Bertot, C. Cohen, M. Kerjean, A. Mahboubi, D. Rouhling, P. Roux, K. Sakaguchi, Z. Stone, P.-Y. Strub, and L. Théry. MathCompAnalysis: Mathematical components compliant analysis library, 2022. Version 0.5.4

2022
[2]

Bousquet, W

N. Bousquet, W. Lochet, and S. Thomassé. A proof of the Erdös-Sands-Sauer-Woodrow conjecture. Journal of Combinatorial Theory, Series B, 137:316–319, 2019

2019
[3]

Chancelier, M

J.-P. Chancelier, M. De Lara, and B. Heymann. Conditional separation as a binary relation. A Coq assisted proof, 2024. Preprint

2024
[4]

De Lara, J.-P

M. De Lara, J.-P. Chancelier, and B. Heymann. Topological conditional separation,
[5]

Doczkal and D

C. Doczkal and D. Pous. Graph theory in Coq: Minors, treewidth, and isomorphisms. Journal of Automated Reasoning, 64:795–825, 2020

2020
[6]

Gale and L

D. Gale and L. S. Shapley. College admissions and the stability of marriage. The American Mathematical Monthly, 69(1):9–15, 1962

1962
[7]

Galeana-Sánchez, R

H. Galeana-Sánchez, R. Rojas-Monroy, and R. Sánchez-López. (A, B)-kernels and Sands, Sauer and Woodrow’s theorem.AKCE Int. J. Graphs Comb., 16(3):284–290, 2019

2019
[8]

Gonthier, A

G. Gonthier, A. Mahboubi, and E. Tassi. A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France, 2016

2016
[9]

N. A. Hamid and C. Castleberry. Formally certified stable marriages. InProceedings of the 48th annual ACM Southeast Conference, pages 1–6, New York, 2010

2010
[10]

Igarashi

A. Igarashi. Coalition formation in structured environments. In Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’17, pages 1836–1837, 2017

2017
[11]

Langlois and F

H. Langlois and F. Meunier. Revisiting classical results on kernels in digraphs, 2025

2025
[12]

Mahboubi and E

A. Mahboubi and E. Tassi.Mathematical Components. Zenodo, Sept. 2022

2022
[13]

T. Nipkow. Gale-Shapley verified.Journal of Automated Reasoning, 68(12), 2024

2024
[14]

Pit-Claudel

C. Pit-Claudel. Alectryonhttps://github.com/cpitclaudel/alectryon
[15]

Sands, N

B. Sands, N. Sauer, and R. Woodrow. On monochromatic paths in edge-coloured di- graphs. Journal of Combinatorial Theory, Series B, 33(3):271–275, 1982

1982
[16]

von Neuman and O

J. von Neuman and O. Morgenstern.Theory of games and economic behaviour. Prince- ton University Press, Princeton, second edition, 1947. 14

1947
[17]

M. Walicki. Resolving infinitary paradoxes.The Journal of Symbolic Logic, 82(2):709– 723, 2017. 15

2017