pith. sign in

arxiv: 2606.05629 · v1 · pith:LBJXLSBJnew · submitted 2026-06-04 · 🧮 math.CO

An automated proof that R(B₈,B₁0)=37

Jeremy Kalfus , Bernard Lidick\'y This is my paper

Pith reviewed 2026-06-28 01:12 UTC · model grok-4.3

classification 🧮 math.CO
keywords Ramsey numberbook graphcomputer-assisted proofgraph theoryformal verificationcombinatorics
0
0 comments X

The pith

The book Ramsey number R(B_8, B_10) equals 37.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper proves that R(B_8, B_10) equals 37. The lower bound was already known, so the contribution is an upper bound showing that every graph on 37 vertices contains either a copy of B_8 or has its complement containing a copy of B_10. The argument was located through an AI-assisted workflow called AutoMath and comes with a Lean formalization of the case analysis. A reader cares because the result pins down the exact value of this specific Ramsey number for book graphs.

Core claim

There exists no graph on 37 vertices that contains neither a copy of B_8 nor has its complement containing a copy of B_10. This rules out any counterexample to the upper bound and therefore establishes R(B_8, B_10) = 37. The proof was discovered using AutoMath and is accompanied by a Lean formalization.

What carries the argument

Exhaustive automated enumeration that rules out all 37-vertex graphs avoiding both B_8 in the graph and B_10 in the complement.

If this is right

  • The exact value of the Ramsey number R(B_8, B_10) is settled at 37.
  • The upper bound is established by showing the non-existence of any avoiding graph on 37 vertices.
  • The combination of automated discovery and Lean formalization confirms the case analysis for this instance.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Automated search methods of this kind could be applied to determine other book Ramsey numbers whose values remain open.
  • The availability of a Lean formalization allows independent verification of the exhaustive search steps.
  • The workflow may extend to related problems in extremal graph theory that involve similar subgraph avoidance conditions.

Load-bearing premise

The automated enumeration has correctly encoded the book graphs and exhaustively checked every possible 37-vertex graph without missing cases or introducing definition errors.

What would settle it

Exhibiting one concrete 37-vertex graph that contains no B_8 and whose complement contains no B_10 would falsify the claimed equality.

Figures

Figures reproduced from arXiv: 2606.05629 by Bernard Lidick\'y, Jeremy Kalfus.

Figure 1
Figure 1. Figure 1: Book graphs B8 and B10. Theorem 1. The book Ramsey number R(B8, B10) is equal to 37. Since the lower bound R(B8, B10) ≥ 37 is already known, it is enough to prove that every graph on 37 vertices contains B8 or its complement contains B10. The argument has two parts. The first part uses structural arguments showing that the hypothetical graph on 37 vertices without B8 or B10 in its complement is strongly re… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript claims that the book Ramsey number R(B_8, B_10) equals 37. The lower bound is taken from the existing literature; the upper bound is established by ruling out the existence of any 37-vertex graph that contains neither a copy of B_8 nor a copy of B_10 in its complement, via an exhaustive search discovered with AutoMath and formalized in Lean.

Significance. If the formalization is faithful to the definitions, the result supplies an exact value for a book Ramsey number. The machine-checked exhaustive search is a clear strength: it is parameter-free, contains no analytic approximations, and directly verifies the non-existence claim against the external definitions of the book graphs. This combination of automated discovery and Lean formalization provides reproducible, high-assurance evidence for the upper bound.

minor comments (2)
  1. [Abstract] The abstract states that the Lean formalization resides in an accompanying repository; the published version should include a stable URL or DOI for the repository to ensure long-term accessibility of the machine-checked proof.
  2. A one-paragraph outline of the main case distinctions or search strategy used in the Lean formalization would help readers connect the informal claim to the verified code without needing to inspect the repository immediately.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive evaluation of the manuscript and for recommending acceptance. Their assessment of the result's significance and the value of the Lean formalization aligns with our own view of the contribution.

Circularity Check

0 steps flagged

No circularity; machine-checked exhaustive search against external definitions

full rationale

The paper establishes the upper bound R(B_8,B_10) ≤ 37 via a Lean-formalized exhaustive case analysis that directly encodes the definitions of book graphs B_8 and B_10 and rules out all 37-vertex graphs lacking either subgraph (or its complement). The lower bound is taken from independent prior literature. No equations, parameters, or ansatzes are fitted or redefined within the paper; the formalization is parameter-free and externally verifiable. No self-citation is load-bearing for the central claim, and the argument does not reduce to any of the enumerated circular patterns. This is a standard computational Ramsey-number proof whose correctness rests on the soundness of the Lean kernel and the completeness of the search, both external to the paper's own text.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof rests on the standard definitions of graphs, induced subgraphs, and book graphs; no free parameters, ad-hoc axioms, or new entities are introduced.

axioms (1)
  • standard math Standard axioms of graph theory and the definition of book graphs B_k as K_{1,k} plus a clique on the k leaves.
    Invoked implicitly when stating the Ramsey number R(B_8, B_10).

pith-pipeline@v0.9.1-grok · 5626 in / 1343 out tokens · 30633 ms · 2026-06-28T01:12:23.974869+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Book Ramsey numbers via algebraic constructions

    math.CO 2026-06 unverdicted novelty 7.0

    Algebraic constructions of strongly regular graphs yield R(B_n,B_n)=4n+1 for infinitely many n and R(B_{n-2},B_n)≤4n-3 for most n, with equality under Hadamard matrix conditions.

Reference graph

Works this paper leans on

19 extracted references · 9 canonical work pages · cited by 1 Pith paper

  1. [1]

    Short proofs in combinatorics and number theory, 2026.arXiv:2603.29961

    Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, and Gregory Valiant. Short proofs in combinatorics and number theory, 2026.arXiv:2603.29961

    arXiv 2026

  2. [2]

    Short proofs in combinatorics, probability and number theory II, 2026.arXiv:2604

    Boris Alexeev, Moe Putterman, Mehtaab Sawhney, Mark Sellke, and Gregory Valiant. Short proofs in combinatorics, probability and number theory II, 2026.arXiv:2604. 06609

    2026

  3. [3]

    Bloom, W

    Noga Alon, Thomas F. Bloom, W. T. Gowers, Daniel Litt, Will Sawin, Arul Shankar, Jacob Tsimerman, Victor Wang, and Melanie Matchett Wood. Remarks on the disproof of the unit distance conjecture, 2026.arXiv:2605.20695

    Pith/arXiv arXiv 2026

  4. [4]

    Axplorer

    AxiomMath. Axplorer. https://github.com/AxiomMath/axplorer. [Accessed 24-04- 2026]

    2026

  5. [5]

    Ellenberg, Adam Zsolt Wagner, and Geordie Williamson

    François Charton, Jordan S. Ellenberg, Adam Zsolt Wagner, and Geordie Williamson. Patternboost: Constructions in mathematics with a little help from ai, 2024.arXiv: 2411.00566

    arXiv 2024

  6. [6]

    doi: 10.1007/978-3-030-79876-5_37

    Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. pages 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. URL:https: //lean-lang.org,doi:10.1007/978-3-030-79876-5_37

    work page doi:10.1007/978-3-030-79876-5_37 2021

  7. [7]

    Rein- forcement learning for graph theory, II

    Mohammad Ghebleh, Salem Al-Yakoob, Ali Kanso, and Dragan Stevanović. Rein- forcement learning for graph theory, II. Small Ramsey numbers.Art Discrete Appl. Math., 8(1):Paper No. 1.07, 7, 2025

    2025

  8. [8]

    Graduate Texts in Mathe- matics

    Chris Godsil and Gordon Royle.Algebraic Graph Theory. Graduate Texts in Mathe- matics. Springer, New York, NY, 2001 edition, April 2001

    2001

  9. [9]

    A. W. Goodman. On sets of acquaintances and strangers at any party.Amer. Math. Monthly, 66:778–783, 1959.doi:10.2307/2310464

    work page doi:10.2307/2310464 1959

  10. [10]

    Jeremykalfus/automath: Initial beta, 2026

    Jeremy Kalfus. Jeremykalfus/automath: Initial beta, 2026. URL:https://github. com/JeremyKalfus/AutoMath,doi:10.5281/ZENODO.19712305

    work page doi:10.5281/zenodo.19712305 2026

  11. [11]

    Small Ramsey numbers for books, wheels, and generalizations.Electron

    Bernard Lidický, Gwen McKinley, Florian Pfender, and Steven Van Overberghe. Small Ramsey numbers for books, wheels, and generalizations.Electron. J. Combin., 32(4):Paper No. 4.64, 20, 2025.doi:10.37236/13577

    work page doi:10.37236/13577 2025

  12. [12]

    URL https://doi.org/ 10.1145/3372885.3373824

    The mathlib Community. The lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20, page 367–381. ACM, January 2020.doi:10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020

  13. [13]

    Alexander Novikov, Ngân V˜ u, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Balog. Alphaevolve: A coding agent for scientific and algo...

    Pith/arXiv arXiv 2025

  14. [14]

    Codex.https://github.com/openai/codex

    OpenAI. Codex.https://github.com/openai/codex. [Accessed 24-04-2026]. 8 JEREMY KALFUS AND BERNARD LIDICKÝ

    2026

  15. [15]

    An openai model has disproved a central conjecture in discrete geometry

    OpenAI. An openai model has disproved a central conjecture in discrete geometry. https://openai.com/index/model-disproves-discrete-geometry-conjecture/. [Accessed 20-05-2026]

    2026

  16. [16]

    Radziszowski

    Stanisław P. Radziszowski. Small ramsey numbers.The Electronic Journal of Combi- natorics, Dynamic Surveys, DS1, 2026.doi:10.37236/21

    work page doi:10.37236/21 2026

  17. [17]

    43 Nature625(7995), 468–475 (2024) https://doi.org/10.1038/s41586-023-06924-6

    Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, PengmingWang, OmarFawzi, PushmeetKohli, andAlhusseinFawzi.Mathematicaldis- coveries from program search with large language models.Nature, 625(7995):468–475, December 2023.doi:10.1038/s41586-023-06924-6

    work page doi:10.1038/s41586-023-06924-6 2023

  18. [18]

    C. C. Rousseau and J. Sheehan. On ramsey numbers for books.Journal of Graph Theory, 2(1):77–87, 1978.doi:10.1002/jgt.3190020110

    work page doi:10.1002/jgt.3190020110 1978

  19. [19]

    William J. Wesley. Lower bounds for book ramsey numbers.Discrete Mathematics, 349(5):114913, May 2026.doi:10.1016/j.disc.2025.114913. https://jeremykalfus.github.ioIndian Springs School, Indian Springs, AL Email address:jeremykalfus@gmail.com Department of Mathematics, Iowa State University, Ames, IA, USA. Email address:lidicky@iastate.edu

    work page doi:10.1016/j.disc.2025.114913 2026