Checking the Ramsey Breakthrough Twice: Isabelle’s 2025 Formalization

Order forced inside a complete graph

Take a collection of vertices and connect every pair. Color each connection either red or blue. The diagonal Ramsey number R(k) is the smallest number of vertices that forces a monochromatic complete subgraph on k vertices, whatever the coloring. A monochromatic triangle means three vertices with all three connecting edges the same color. It does not require the other connections from those vertices to have that color. The requirement concerns one internally consistent subset hidden inside a potentially messy whole.

Here is a complete small example. In a graph with six vertices, select one vertex v. Among its five incident edges, at least three have the same color. Suppose v connects in red to a, b, and c. If any edge among a, b, c is red, it completes a red triangle with v. If none is red, those three edges are blue and a, b, c form a blue triangle. Reversing the color names handles the other case. Thus six vertices suffice to force a monochromatic triangle.

An exponential improvement can matter without exact numbers

Five vertices do not suffice in that example. Arrange them around a pentagon, color its five sides red, and color the five diagonals blue. The red edges form a cycle of length five, which has no triangle. The blue edges also form a cycle of length five, visited in a different order. This proves R(3) = 6 together with the previous argument. Larger k quickly escape such hand-sized constructions, and upper and lower bounds become the main way to understand the landscape.

The breakthrough gives an exponential upper bound with a base strictly below four for sufficiently large k. To appreciate the phrase, use an illustrative base of 3.99 without attributing that particular number to the theorem. Relative to 4 to the power k, the ratio is (3.99 divided by 4) to the power k. The improvement repeats at every factor, so a small change in the base eventually dominates any fixed multiplicative constant. That explains the mathematical importance of an exponential improvement while avoiding a misleading claim about exact values for small k.

The diagonal restriction also deserves its name. A two-parameter Ramsey number asks for either a red complete subgraph on s vertices or a blue one on t vertices. Putting s = t = k produces the diagonal case. Allowing different target sizes can be useful inside a proof even when the final question is symmetric. For example, a restriction to the red neighbors of a vertex has already secured one red connection, so the remaining red target can shrink while the blue target stays unchanged. Tracking this asymmetry is a way to retain information that a single-size description would discard.

Why a graph proof starts tracking real quantities

A basic recursive approach selects a vertex and separates its neighbors according to the color of the connecting edge. One can then search within one of those sets for a smaller monochromatic structure. Stronger bounds need to extract more information than the bare size of the two sets. Edge density, meaning the fraction of available pairs carrying a chosen color, records how favorable a region remains as the argument repeatedly restricts attention to smaller vertex collections.

Density is a rational number for a finite graph, but inequalities governing many stages naturally introduce logarithms, entropy-like expressions, and real parameters. A proof might trade a decrease in available vertices for an increase in density, much as a budget tracks both the cost and benefit of a sequence of choices. This paragraph is an explanatory model of why such mathematics appears, rather than a replacement for the published algorithm. The formalization has to retain all the hypotheses that make those trades legitimate at each stage.

A decimal is evidence only when its error is controlled

Paulson identifies computer algebra as an unexpectedly substantial part of the development. The Isabelle proof uses checked methods for differentiation, asymptotic reasoning, and interval arithmetic. That combination matters because the graph-theoretic construction ultimately needs strict inequalities. A graph argument can be completely convincing up to its final numerical estimate and still fail if a rounding error changes the sign of a tiny margin. A proof assistant must connect each such estimate to the exact expression under consideration.

For an independent miniature example, consider q(x) = x times (1 minus x) on the interval from zero to one. Rewriting it as one quarter minus (x minus one half) squared proves q(x) is at most one quarter everywhere. Sampling at a thousand points does not by itself prove the same claim between sample points. More complicated functions may need interval enclosures: a computation returns guaranteed lower and upper bounds valid for every argument in a subinterval. Splitting the interval can tighten an enclosure, but the logical guarantee comes from the proved arithmetic rules, not from the plot looking smooth.

The phrase sufficiently large hides an important dependency

An asymptotic bound makes a quantified promise. For every integer k beyond some threshold, the inequality holds. It does not necessarily give a small or optimized threshold. A statement involving an auxiliary parameter requires additional care: a threshold valid for each fixed parameter need not work uniformly for every parameter in an interval. Swapping those quantifiers without justification can create a gap even when every displayed limit is individually correct.

For example, the sequence x to the power n tends to zero for each fixed x between zero and one. Yet no single n makes it smaller than one half for every x strictly below one, because x can be chosen sufficiently close to one. Restrict x to the closed interval from zero to three quarters and the same bound becomes uniform: every such power is at most (3/4) to the power n. This original example explains why endpoint conditions and compact parameter ranges deserve explicit attention when turning an asymptotic combinatorial argument into formal mathematics.

Independent systems give different kinds of evidence

The Isabelle account acknowledges its debt to the earlier Lean development while reporting a distinct formalization. That is stronger evidence than rerunning the same checker twice, because different libraries, logical foundations, and proof organization can expose different missing assumptions. It is not perfect independence: both formalizations address the same mathematical argument, and both still require faithful statements and trustworthy implementations. A reader should ask what was independently reconstructed and what was borrowed, rather than compressing every form of checking into one universal stamp of certainty.

The useful long-term artifact is a network of graph definitions, analytic lemmas, and checked estimates that can be changed and tested. Improving a parameter may require revisiting an earlier inequality; a formal development reveals the affected dependencies instead of silently assuming the old proof still works. That makes formalization a possible research instrument as well as a verification method. As of the October 2026 cutoff, this article makes no claim that the Isabelle development has produced a new optimal Ramsey bound. Its demonstrated contribution is a checkable treatment of a recent breakthrough and an unusually clear account of the numerical work that treatment requires.