Is there a graph on 40 vertices with no triangle and no 10 vertices that are all unconnected?

Among any 41 people there are always 3 mutual friends or 10 mutual strangers, and among 39 that can fail. Whether 40 is enough is still open: the answer, 40 or 41, is one of the best-known unknown values in combinatorics.

Ramsey's theorem (1930) says that order appears in any large enough system: among enough people there are always k mutual friends or l mutual strangers. The smallest such number is the Ramsey number R(k,l). Only a handful are known exactly: R(3,9) = 36 was settled in 1982 and the last classical value, R(4,5) = 25, in 1995.

For R(3,10) the bounds have closed in on two values. Exoo found a 39-vertex graph in 1989 that gives R(3,10) at least 40, and Angeltveit proved in 2024 that it is at most 41. One graph on 40 vertices with no triangle and no 10 independent vertices would settle it as 41; proving that none exists would settle it as 40.

The lab searches for such a graph among graphs with symmetry, class by class, with a SAT solver whose every no answer comes with a proof that a separate program checks.

Where it stands Just started: building a SAT search with checked proofs over every symmetry class of a 40-vertex candidate.