Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalising New Mathematics in Isabelle: Diagonal Ramsey

Lawrence C Paulson

TL;DR

The paper reports a complete Isabelle/HOL formalisation of Campos et al.'s exponential-bound result for Ramsey numbers, a landmark contemporary theorem. It introduces the improved book algorithm, partitions the vertex set into $X$ and $Y$, and uses a hierarchy of locale-based formal modules to manage the intricate state and invariants; the development relies heavily on computer algebra for real-analytic estimates, derivatives, and high-precision numerics. The author details the key lemmas and their formal proofs, including Lemma 4.1 and the zigzag lemma, and progresses through far-from-diagonal and near-diagonal regimes to establish $R(k) \le (4-\epsilon)^k$ with a rigorous, machine-checked argument. The work demonstrates that proof assistants can handle new, technically dense mathematics and produce a verifiable, tunable foundation for potential improvements and future refinements, bridging formalised and traditional mathematical practice.

Abstract

The formalisation of mathematics is starting to become routine, but the value of this technology to the work of mathematicians remains to be shown. There are few examples of using proof assistants to verify brand-new work. This paper reports the formalisation of a major new result (arXiv:2303.09521) about Ramsey numbers that was announced in 2023. One unexpected finding was the heavy need for computer algebra techniques.

Formalising New Mathematics in Isabelle: Diagonal Ramsey

TL;DR

The paper reports a complete Isabelle/HOL formalisation of Campos et al.'s exponential-bound result for Ramsey numbers, a landmark contemporary theorem. It introduces the improved book algorithm, partitions the vertex set into and , and uses a hierarchy of locale-based formal modules to manage the intricate state and invariants; the development relies heavily on computer algebra for real-analytic estimates, derivatives, and high-precision numerics. The author details the key lemmas and their formal proofs, including Lemma 4.1 and the zigzag lemma, and progresses through far-from-diagonal and near-diagonal regimes to establish with a rigorous, machine-checked argument. The work demonstrates that proof assistants can handle new, technically dense mathematics and produce a verifiable, tunable foundation for potential improvements and future refinements, bridging formalised and traditional mathematical practice.

Abstract

The formalisation of mathematics is starting to become routine, but the value of this technology to the work of mathematicians remains to be shown. There are few examples of using proof assistants to verify brand-new work. This paper reports the formalisation of a major new result (arXiv:2303.09521) about Ramsey numbers that was announced in 2023. One unexpected finding was the heavy need for computer algebra techniques.
Paper Structure (15 sections, 11 theorems, 17 equations, 3 figures)

This paper contains 15 sections, 11 theorems, 17 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Ramsey's theorem
  3. The improved Ramsey algorithm
  4. Defining the book algorithm in Isabelle
  5. A detailed peek at a proof
  6. A progression of theorems
  7. On red and density-boost steps
  8. Bounding the size of $Y$
  9. Bounding the size of $X$
  10. The zigzag lemma
  11. An exponential improvement far from the diagonal
  12. An exponential improvement a little closer to the diagonal
  13. Concluding the proof of the main theorem
  14. Formal reasoning about computer algebra
  15. Discussion and conclusions

Key Result

Theorem 1

For all $k$ and $\ell$ there exists a number $R(k,\ell)$ such that if the edges of a complete $R(k,\ell)$-graph $G$ are coloured red or blue, then $G$ will contain either a red $k$-clique or a blue $\ell$-clique.

Figures (3)

  • Figure 1: An example to illustrate $R(3,3)=6$. Solid lines are red. Two cliques can be seen.
  • Figure 2: An algorithm for proving Ramsey's theorem. (The hollow colour is blue.)
  • Figure 3: The Book Algorithm. (The hollow colour is blue.)

Theorems & Definitions (11)

  • Theorem : Ramsey
  • Lemma : 4.1
  • Lemma : 6.1
  • Lemma : 7.1
  • Theorem : 9.1
  • Lemma : 9.2
  • Theorem : 10.1
  • Lemma : 10.2
  • Theorem : 11.1
  • Theorem : 1.1
  • ...and 1 more