Pith. sign in

REVIEW 2 minor 1 cited by

An automated proof that R(B_8,B_10)=37

T0 review · 0 major / 2 minor · reviewed 2026-06-28 · grok-4.3

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The book Ramsey number R(B_8, B_10) equals 37.

desk verdict They've closed R(B_8, B_10)=37 with a Lean-formalized exhaustive search for the upper bound. read the letter →

arxiv 2606.05629 v1 pith:LBJXLSBJ submitted 2026-06-04 math.CO

Jeremy Kalfus , Bernard Lidický This is my paper · ORCID
classification math.CO
keywords Ramseynumberbookgraphcomputer-assistedprooftheoryformalverificationcombinatorics
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

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.

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.

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.

Watch

Extended reading notes

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.

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.

Editorial extensions

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.

Reading between the lines

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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

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 · score 0.0 of 10

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.

Assumptions & free parameters 0 free parameters · 1 assumptions · 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.

assumptions (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).

how reviews work

0 comments
Cite this review

Pith. "Pith review of An automated proof that R(B_8,B_10)=37." pith.science (2026). https://pith.science/paper/LBJXLSBJ

@misc{pith2026260605629,
  author       = {Pith},
  title        = {Pith review of: An automated proof that R(B_8,B_10)=37},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LBJXLSBJ}},
  note         = {Machine review of arXiv:2606.05629}
}
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.

Figures

Figures reproduced from arXiv: 2606.05629 by the authors.

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 regular. In … view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. Book Ramsey numbers via algebraic constructions

    math.CO 2026-06 unverdicted novelty 7.0 of 10

    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 · 13 canonical work pages · cited by 1 Pith paper

  1. [1]

    Alexeev, M

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

    work page 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]

    Remarks on the disproof of the unit distance conjecture

    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

    work page Pith review arXiv 2026

  4. [4]

    Axplorer

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

    2026

  5. [5]

    PatternBoost: Constructions in Mathematics with a Little Help from AI

    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

    work page Pith review arXiv 2024

  6. [6]

    The Lean 4 Theorem Prover and Programming Language

    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

Show all 19 references
  1. [9]

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

    1959 doi

  2. [10]

    Jeremykalfus/automath: Initial beta, 2026

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

    2026 doi

  3. [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

    2025 doi

  4. [12]

    The lean mathematical library

    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

    2020 doi

  5. [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, Push...

    2025 arXiv

  6. [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

  7. [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

  8. [16]

    Radziszowski

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

    2026 doi

  9. [17]

    Pawan Kumar, Emilien Dupont, Francisco J

    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 lan...

    2023 doi

  10. [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

    1978 doi

  11. [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 St...

    2026 doi

Pith tools

Reviewed June 28, 2026 · model on record in the stance chip above.