[2606.05629] An automated proof that R(B_8,B_10)=37
Abstract:We present a short proof that the book Ramsey number $R(B_8,B_{10})$ equals 37. The lower bound $R(B_8,B_{10}) \ge 37$ is already available in the literature, so it is enough to rule out a 37-vertex graph containing neither a copy of $B_8$ nor a copy of $B_{10}$ in its complement. The problem as well as the proof were found with AutoMath, an AI-assisted mathematical discovery workflow developed by the first author. A Lean formalization of the upper-bound argument is available in the accompanying repository.
View PDF HTML (experimental) Abstract:We present a short proof that the book Ramsey number $R(B_8,B_{10})$ equals 37. The lower bound $R(B_8,B_{10}) \ge 37$ is already available in the literature, so it is enough to rule out a 37-vertex graph containing neither a copy of $B_8$ nor a copy of $B_{10}$ in its complement. The problem as well as the proof were found with AutoMath, an AI-assisted mathematical discovery workflow developed by the first author. A Lean formalization of the upper-bound argument is available in the accompanying repository. Comments: 8 pages Subjects: Combinatorics…
saved by
related reading
- Off-diagonal Ramsey numbersarxiv.org
- Ramsey theory and strength of graphsarxiv.org
- [2305.02725] Two-round Ramsey games on random graphsarxiv.org
- Interlacing Families IV: Bipartite Ramanujan Graphs of All Sizesarxiv.org
- cs.stanford.edu/~knuth/papers/claude-cycles.pdfcs.stanford.edu
- Forbidding Exactly One Hamming Distancearxiv.org
- Induced rational exponents near twoarxiv.org
- [2602.05192] First Proofarxiv.org
- Shtetl-Optimized >> Blog Archive >> Ten Signs a Claimed Mathematical Breakthrough is Wrongscottaaronson.blog
- [2510.01346] Aristotle: IMO-level Automated Theorem Provingarxiv.org
- [2603.23431] On the number of families avoiding a subposetarxiv.org
- unit-distance-remarks.pdfcdn.openai.com