Improvements to the Diagonal Ramsey Upper Bound

We present a world record - a significant improvement to a famous unsolved problem in math proposed by Paul Erdős in 1935. This was achieved by a swarm of AI agents working on it together over a weekend hackathon, and our result is verified in Lean. Our result does not in any way depend on the recent manuscripts published by OpenAI.

We’ll release details on the 14 open problems we solved in the same hackathon next week.

The Diagonal Ramsey Problem

The problem in question is the diagonal Ramsey numbers. Take a set of points, connect every pair with a line, and colour each line red or blue. The Ramsey number is the smallest number of points at which every possible colouring is forced to contain a shape drawn in a single colour, with every corner of the shape joined to every other.

For a triangle, that number is six. After that, exact answers quickly become impossible to compute: the number of possible colourings explodes so fast that by the pentagon, checking them all would take more steps than there are atoms in the universe. The answer for the triangle and the square is known, but even the pentagon remains unsolved. So instead of exact answers, mathematicians ask how fast the number of points grows as the shapes get bigger.

In 1935, Erdős and Szekeres showed that each new shape needs at most about four times as many points as the one before, which stood for 88 years.

Result

Our proof builds on a method introduced in 2023 by Campos, Griffiths, Morris and Sahasrabudhe, the first to beat Erdős and Szekeres’s 1935 bound. Their approach narrows a large network down to smaller groups step by step. Gupta, Ndiaye, Norin and Wei tuned this method to reach 3.8ᵏ, and Lu and Wang 2026 refined it further to reach 3.695ᵏ. Our agents describe their new techniques as follows:

1. Row-moment potential. Every proof in this line so far scored a group by its average number of connections. We gave extra weight to the most strongly connected members instead, which reveals progress that an average hides, and this one change accounts for most of our gain.
2. Fractional row weight. The score multiplies together the sizes of two groups, and earlier proofs counted both at full weight. We count one of them only partly, so shrinking that group costs less and the search can take larger steps without losing ground.
3. Self-improving feedback bank. The method also relies on a list of already-proven results about lopsided versions of the problem, which Lu and Wang supplied and kept fixed; they also showed that a fixed list can never get much below 3.69ᵏ. Our method improves some of those results, so we put the improved versions back into the list and reuse them, round after round, with a computer checking every step exactly.

We verified our result is correct with Formal Verification, a technique that converts our math proof into a logical programming language called Lean. This offers us the guarantee that our mathematical reasoning is correct and not hallucinated. However, the problem may have been incorrectly translated by our Agents, as humans have not reviewed this, which is the main risk to this solutions correctness. However, this risk is mitigated as we build on prior work that formalised the same problem.

The proof is exceptionally large at 5M lines of Lean, second only to Anthropic’s Fermat’s Last Theorem project and larger than any of the proofs in OpenAI’s recent release. This is because we perform a grid search over 100k+ possible values and each of these values is a single Lean file. We heavily relied on Lu-Wang’s project that provided a scaffold to build on.

Engineering

We created an auto-researcher that combined several models, harnesses, tools, and indexes to accelerate mathematical discovery. The agents were instructed to contribute ideas, mathematically prove them, critique each other's work, and formally the most promising approaches in Lean.

The agents were predominantly orchestrated by Devin with GPT-6 Astra and Claude Opus 5.5. Although, as our agents were decentralised, several other agent harnesses were collaborating and communicating with each other including CodeX, ClaudeCode, and cursor.

Most ideas were rejected quickly, however there were significant resources spent on a long tail of several rejected long running ideas.

The Lean check took 4 hours on a r7a.24xlarge with 96 CPU cores and 768GB of memory. There’s certainly utilisation and Lean line length improvements that could reduce the resources required to formally verify this finding.