Open problems, settled by computer

New exact values of small Ramsey and Rado numbers

Seven values that were known only as ranges, or left blank in published tables, settled with SAT solvers. Every "no colouring exists" claim comes with a proof that was checked line by line by cake_lpr, a formally verified checker. Papers and data are on Zenodo. They have not been peer reviewed yet.

Values settled

Combined paper: 3 November 2026

Five small Ramsey numbers for fans and complete bipartite graphs

R(F₄, F₄) was 18–24→18
ValuePreviously knownSettled
R(F₄, F₄) (fan of 4 triangles vs 4)18–2418
R(F₃, F₅) (fan of 3 triangles vs 5)21–2621
R(F₄, F₅) (fan of 4 triangles vs 5)22–2822
R(K₃,₃, K₃,₄) (complete bipartite)19–2019
R(K₂,₄, K₃,₅) (complete bipartite)19–2019

For all five, the new part is the upper bound. The lower bounds were already known: R(F₄, F₄) ≥ 18 and R(F₄, F₅) ≥ 22 follow from Zhang, Broersma and Chen (Bull. Aust. Math. Soc. 92 (2015) 19–23). The two bipartite values were listed as "19–20" in Table IVb of Radziszowski's dynamic survey Small Ramsey Numbers.

Each upper bound is a SAT instance shown unsatisfiable, split into cases by the maximum degree of one colour, with symmetry breaking inside each case. For R(F₄, F₄) there are 2153 colourings of K₁₈; the proofs total 1.27 GB. For R(F₄, F₅), the cases with few red edges did not finish when split by red degree, so the remaining cases were re-split by blue degree; all six cases are unsatisfiable, and the proofs total about 63 GB. All LRAT proofs pass cake_lpr.

We also re-verified R(F₃, F₄) = 17, first published by Jiang and Shao (arXiv:2610.26109, 19 October 2026), using two independent encodings.

When informed of R(F₄, F₄) = 18, Professor Stanisław Radziszowski, who has maintained the survey since 1994, replied: "The exact value you obtain, 18, is surprisingly low for F4, but I am used to surprises in Ramsey theory." He said he would cite it as appropriate in the next revision of the survey (29 October 2026).

Correction (1 November 2026): the first versions stated that the lower bounds R(F₄, F₄) ≥ 18 and R(F₄, F₅) ≥ 22 were new. They were already known from Zhang–Broersma–Chen (2015). Only the upper bounds are new. The Zenodo records were revised accordingly (version 2).

Not yet peer reviewedAll proofs checked by cake_lpr
Combined paper (Zenodo) R(F₄,F₄) paper and data Four values: paper and data

28 October 2026

Four-colour Rado numbers R₄(4(x−y)=3z) = 313 and R₄(5(x−y)=2z) = 625

Colour the integers 1 to n with four colours. For n = 313, every colouring contains x, y, z of one colour with 4(x−y) = 3z; for n = 312 there is a colouring that avoids it. The smallest such n is the Rado number.

Table entry was blank→313625= 5⁴

Both were blank in Table 10 of Chang, De Loera and Wesley (ISSAC 2022, arXiv:2210.03262). 625 equals 5⁴, which hints that the three-colour pattern "the answer is a⁴ when a ≥ b + 2" may extend to four colours.

Lower bounds are explicit colourings checked by a separate program. Upper bounds are unsatisfiability proofs checked by cake_lpr; large instances were split by cube-and-conquer, and the cube split was checked for completeness. 313 and 625 were also confirmed with the colour-symmetry breaking removed.

Not yet peer reviewed19 proofs checked by cake_lpr
Paper and data (Zenodo)

Values first published by others, independently confirmed

ValueFirst published byWhat we did
R(F₃, F₄) = 17Jiang and Shao (arXiv:2610.26109, 19 Oct 2026)Confirmed with a single unsplit encoding and with a case split
R₄(2(x−y)=3z) = 226Ichikawa (Zenodo, 22–23 Oct 2026)Our computation finished in July but was published later. Confirmed without symmetry breaking and with a verified checker, the two gaps the original author listed

An attempt that did not succeed

Searching for a counterexample to the Erdős–Gyárfás conjecture (August 2026, stopped)

The conjecture says every graph with minimum degree 3 contains a cycle whose length is a power of 2. Restricting to cubic graphs, the SAT search found no counterexample up to 32 vertices. The proofs were not exported and independently checked, so we do not claim this as settled. Simulated annealing could never remove the last cycle of length 16. We had decided to stop if no counterexample appeared, and we stopped.

No counterexample foundResults up to 32 vertices not proof-checked

How every result is checked the same four steps each time

1. Lower bound by an explicit exampleAn avoiding colouring is checked by a separately written program, and we confirm the checker catches a deliberately broken copy.
2. Upper bound by SATAll colourings are encoded as a formula and shown unsatisfiable. Symmetry breaking cuts years of search to minutes or hours.
3. Proof checked by cake_lprThe solver writes out its full proof, which the formally verified checker cake_lpr verifies line by line, so the solver itself need not be trusted.
4. The encoding re-read independentlyA separate program re-reads each formula to confirm it encodes the problem, and known small values are reproduced the same way.

Next candidates open; not currently running

ProblemKnown rangeStatus
Book Ramsey number R(B₄, B₇)22–23Not yet attempted
Fan Ramsey number R(F₅, F₅)23–30Searches for a K₂₃ colouring did not finish within our time limit; stopped
Bipartite R(K₂,₅, K₂,₈)22–23A three-day run at n = 22 did not finish; stopped

Use of AI

The search code, the computations and the paper drafts were made together with an AI agent (Claude Code), as stated in the acknowledgements of each paper. To avoid trusting the AI's answers as they are, every result goes through the four checks above.