Improved bounds for the smallest 4-chromatic graph of girth six

Glauco Rampone

REVIEW 1 major objections 6 minor 19 references

Improved bounds for the smallest 4-chromatic graph of girth six

T0 review · 1 major / 6 minor · reviewed 2026-08-28 · deepseek-v4-flash

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

Pith's one-line read The smallest 4-chromatic graph of girth 6 lies between 29 and 64 vertices.

desk verdict A strong, honest narrowing of n6(4) to [29,64]: the 64-vertex witness is formally verified in Lean, and the lower-bound search is credible and transparently documented. read the letter →

arxiv 2608.23652 v1 pith:J5SGXRXA submitted 2026-08-24 math.CO cs.DM

Glauco Rampone This is my paper · ORCID

classification math.COcs.DM MSC 05C1505C3805C2505C8568V20

keywords chromaticnumbergirthcriticalgraphsCayleyvoltageSATmodulosymmetriesformalverificationLean

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

This paper narrows the size of the smallest 4-chromatic graph of girth 6 to between 29 and 64 vertices, down from the previous 26 to 66. On the upper side it gives an explicit 64-vertex graph with 152 edges: girth exactly 6, needing four colours, and critical in both the vertex and edge senses. On the lower side a computer exhaustion proves that every graph of girth at least 6 on 28 or fewer vertices is 3-colourable. The combined result leaves a 36-vertex window for the true extremal value, and the upper-bound witness is checked inside a proof assistant, so its non-3-colourability does not rest on trust in one program.

What carries the argument

The upper bound rests on an explicit construction: G64 is the graph on Z_64 whose 152 edges are the union of 20 orbits of pairs under the map v -> v+8, a semiregular cyclic action lifting an 8-vertex base multigraph (a voltage graph). The lower bound rests on a reduction to 4-critical graphs: any counterexample on at most 28 vertices would contain a 4-critical subgraph with at least (5n+2)/3 edges by the Liu-Postle density bound, so the search confines itself to graphs meeting that edge count. The search is executed in the SAT modulo symmetries framework with co-certificate learning, which prunes partial adjacency matrices by isomorphism and learns clauses forbidding any graph that admits a 3-colouring. For the upper bound, non-3-colourability is additionally certified in the Lean proof assistant by re-traversing a 219,532-node refutation certificate under a machine-checked soundness theorem.

What would settle it

Exhibit a graph of girth at least 6 on 28 or fewer vertices with chromatic number 4 (refutes Theorem 2), or find a proper 3-colouring, or a cycle of length 3, 4, or 5, in the deposited 64-vertex graph (refutes Theorem 1).

Watch

Extended reading notes

Core claim

This paper establishes two new bounds on n6(4), the minimum order of a 4-chromatic graph of girth 6: at least 29 vertices, and at most 64. The upper bound is witnessed by an explicit graph G64 with 64 vertices and 152 edges whose girth is exactly 6 and whose chromatic number is exactly 4; it is vertex- and edge-critical, has independence number 24, and its automorphism group is cyclic of order 8 acting semiregularly. The lower bound is a computational proof that every graph of girth at least 6 on at most 28 vertices is 3-colourable, obtained by an exhaustive isomorph-free search over 4-critical candidates in the SAT modulo symmetries framework. The paper also proves structural obstructions: no smaller witness arises by local modifications of either known witness, no 4-chromatic Cayley graph of girth 6 exists on 54-63 vertices, and no witness on at most 63 vertices admits a semiregular automorphism group with two or three vertex orbits.

Load-bearing premise

The lower bound assumes the computer search that rules out graphs on 27 and 28 vertices is correct; a hidden bug in the solver, the symmetry-breaking, or the encoding could hide a counterexample, and the paper supplies no machine-checked proof for those two runs.

Editorial extensions

If this is right

If Theorem 1 stands, a 64-vertex graph with girth 6 and chromatic number 4 exists, so any future attempt to lower n6(4) below 64 must beat this explicit witness.
If Theorem 2 stands, every graph with girth at least 6 on 29 or fewer vertices is 3-colourable, so the exhaustive search for a smaller witness must start at 29 vertices.
The lower-bound method, validated against known values n4(4)=11 and n5(4)=21, makes the n=28 exhaustion feasible on one consumer core and opens the door to n=29.
Structural obstructions rule out Cayley graphs on 54-63 vertices and any semiregular symmetry with two or three orbits on at most 63 vertices; a smaller witness, if it exists, must be essentially asymmetric.
The Lean-certified refutation certificate for G64 converts a 219,532-node search tree into machine-checkable evidence, a standard of proof rarely attached to extremal graph records.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Inference: the steep cost growth per order (a factor up to 9.6 at the last step) makes pushing the exhaustion to n=29 a matter of weeks, but reaching the 54-63 range infeasible; the author stops short of conjecturing that n6(4)=64, and the symmetric dead ends below 64 leave an asymmetric witness as a live possibility.
Inference: a smaller asymmetric witness, if one exists, would not show up in the semiregular lift searches; the paper's own randomized asymmetric searches are non-exhaustive, so the true value could still be well below 64.
Inference: the co-certificate learning method, coupled with the 4-critical density reduction, could accelerate other extremal graph searches where the obstruction is chromatic number and girth, not just this record.
Inference: the lower bound is currently less trustworthy than the upper bound because the former lacks a machine-checked certificate; the announced pipeline for formally verified SMS runs could close that gap and would make the 29 lower bound as convincing as the 64 upper bound.

Share X Bluesky LinkedIn Reddit HN

Formalized claims in Lean

Claim #1: This paper establishes two new bounds on n6(4), the minimum order of a 4-chromatic graph of girth 6: at least 29 vertices, and at most 64. The upper bound is witnessed by an explicit graph G64 with 64 vertices and 152 edges whose girth is exactly 6 and whose chromatic number is exactly 4; it is vertex- and edge-critical, has independence number 24, and its automorphism group is cyclic of order 8 a

/-- @claim 1 This paper establishes two new bounds on n6(4), the minimum order of a 4-chromatic graph of girth 6: at least 29 vertices, and at most 64. The upper bound is witnessed by an explicit graph G64 with 64 vertices and 152 edges whose girth is exactly 6 and whose chromatic number is exactly 4; it is vertex- and edge-critical, has independence number 24, and its automorphism group is cyclic of order 8 a -/
def central_claim : Prop :=

Signed reviews

No signed human review yet.

Request a human review

A listed scientist reviews the paper for a fee and the review publishes here regardless of verdict. See the reviewers or get listed.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

You should read this if you care about extremal graph theory records or formal verification of computational combinatorics. The paper improves both bounds on n6(4) from [26,66] to [29,64]. The upper bound is an explicit 64-vertex graph G64, and the non-3-colourability is genuinely machine-checked: a 219,532-node refutation certificate is re-validated inside Lean 4 with a soundness theorem. That is above the usual standard for this literature, and it earns real credit.

The lower bound, n6(4) >= 29, is an exhaustive SMS search with co-certificate learning, using a reduction to 4-critical graphs and the Liu–Postle density bound. The computation is not end-to-end machine-checked, and the paper says so plainly in Remark 4. That is the main soft spot. A bug in the propagator, the encoding, or the co-certificate mechanism could in principle let the search miss a 27- or 28-vertex counterexample. The validation is strong: the pipeline re-derives the old bound n6(4) >= 26 on orders 14–25, matches n4(4)=11 and n5(4)=21, and the two new orders were rerun in audited form on a different machine. I would not call the lower bound load-bearing on a single untrusted artifact; the paper's transparency and multiple cross-checks put it well within the normal envelope of computational combinatorics. The missing certificate is a limitation, not a fatal flaw.

There is a small proof slip near the start of Section 5: the claim that the balls of radius 2 around the endpoints of an edge are disjoint trees is false (they overlap at the endpoints and beyond). The bound n' >= 14 is still correct via the standard Moore-type argument, so this is easily fixed in revision and does not affect the search results.

The structural obstructions in Section 6 are a nice complement, especially the Cayley and semiregular-type exclusions. They are clearly explained and backed by the deposited logs.

Who should engage: anyone working on small chromatic graphs, SAT-based graph generation, or formal verification of computer-assisted proofs. The paper is honest about what is verified and what is not, and the artifacts are all available.

My bottom line: send it to peer review. A serious referee should look at the search logs, the Lean file, and ask for a corrected proof of the n' ≥ 14 bound. The result is likely to stand, and the upper bound verification sets a good precedent for the field.

Referee Report

1 major / 6 minor

Summary. The paper studies n_6(4), the minimum order of a 4-chromatic graph of girth at least 6. It improves the previous bounds 26 ≤ n_6(4) ≤ 66 to 29 ≤ n_6(4) ≤ 64. The upper bound is witnessed by an explicit graph G64 on 64 vertices with 152 edges, with girth exactly 6, chromatic number 4, vertex- and edge-critical, and automorphism group cyclic of order 8; all claims about G64 are verified by independent programs and, for non-3-colourability, by a formally verified Lean 4 checker with a machine-checked soundness theorem. The lower bound is established by an exhaustive isomorph-free SAT-modulo-symmetries computation with co-certificate learning over 4-critical candidates for orders 14–28, validated by re-deriving known values and by audited reruns. The paper also proves structural obstructions: no smaller witness arises from the known witnesses by local modifications, no Cayley graph on 54–63 vertices is 4-chromatic of girth 6, and no graph on at most 63 vertices with a semiregular automorphism group of two or three vertex orbits is a witness.

Significance. If correct, this is a clean improvement of a longstanding record, and it narrows the remaining gap substantially. The upper-bound witness is remarkably well documented: the Lean 4 formalization, including a soundness theorem for the certificate checker, is an unusually high standard for record graphs and makes Theorem 1 reproducible in minutes. The lower-bound computation is also carefully audited: it re-derives the previous lower bound by a disjoint method, matches n_4(4)=11 and n_5(4)=21, and records full logs and hashes. The structural results are valuable in ruling out the most symmetric routes to a smaller witness. The paper is honest about the epistemic asymmetry between the two theorems (Remark 4).

major comments (1)

[§5, Theorem 2 and Remark 4] The lower bound n_6(4)≥29 rests on the correctness of the SMS framework [10], the co-certificate learning mechanism [11], and the authors' propositional encoding. The paper provides validations against known values and audited reruns, but there is no end-to-end machine-checked certificate for the new orders n=27 and n=28; a single false-negative bug in the propagator, the co-certificate clause learning, or the encoding could make the UNSAT results unsound. Because Theorem 2 is half of the main result, this is a load-bearing gap. I request either (i) a second, independently implemented enumeration for n=27 and n=28, or (ii) a formally checked certificate along the lines of [12,13], or (iii) at minimum a detailed written proof of the completeness of the encoding and of the co-certificate learning, explaining why no learned clause can exclude a non-3-colourable graph and why the recursion cutoff in the minimality checker cannot cause a false negative.

minor comments (6)

[§5 and §6] The sentence 'the balls of radius 2 around the two endpoints of any edge are disjoint trees' is not literally true, since each radius-2 ball contains the other endpoint; the intended standard Moore-bound argument counts the two rooted trees at the endpoints after removing the edge uv. Please rephrase in Section 5 and in the analogous statement in Proposition 6.
[§6, Proposition 7] The text says 'This gives 106 pairs' after counting '66 isomorphism classes of orders 15–31 at r=2 and the 40 classes of orders 10–21 at r=3'; these counts sum to 105. Please check the count or clarify the discrepancy.
[§6, Proposition 5] The statement that the same rigidity phenomena hold for the 66-vertex graph of [3] is less detailed than the treatment of G64; please specify exactly which items (i)–(iii) were re-verified for that graph.
[§6, Proposition 7] The fibre-deletion induction that discharges the minimum-degree constraint is sketched in a few lines; a more explicit statement of why a fibre of degree ≤2 is disjoint from every 4-critical subgraph would improve readability.
[§1] The statement that 'every known witness of an n_g(4) record with g≥6' includes the 171-vertex graph 'described there as LCF graphs' could be clarified by specifying the semiregular group action and orbit count for that graph.
[§3] The sentence 'the deposited code now uses the sharper girth-5 bound (5n+2)/3 of Liu and Postle [9]' is a bit unclear about which code version produced G64; please clarify whether the 152-edge candidate passes both bounds.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: explicit construction, external exhaustion, and independent verification.

full rationale

The paper's central claims are an explicit upper-bound witness G64 (Theorem 1) and a computational lower bound via exhaustive isomorph-free search (Theorem 2). Neither claim reduces to its inputs by construction. G64 is defined concretely by edge orbits; its girth, chromatic number, criticality, independence number, and automorphism group are verified by multiple independent programs and, for the chromatic number and girth facts, by a formally verified Lean checker with a soundness theorem. There are no fitted parameters renamed as predictions. The lower-bound search uses the SMS framework and co-certificate learning from external prior work by other authors (Kirchweger, Peitl, Szeider), and it imports the Liu–Postle edge-density bound, which is an external theorem not derived from the target result. The reduction to 4-critical graphs is a standard, logically valid argument. Validation against known values (n4(4)=11, n5(4)=21) and re-deriving n6(4)>=26 by a disjoint method are independent checks, not circular inputs. The paper honestly flags in Remark 4 that no machine-checked certificate for the n=27 and n=28 runs is yet provided; that is a matter of proof assurance, not circularity, and the self-citation concern does not arise because the author does not rely on their own prior work for the load-bearing steps. The structural obstructions are exhaustive computations or simple arguments with external classical references. Thus the derivation chain is self-contained and no circular step is present.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claims rest on standard external theorems (Liu-Postle density bound, group classification) and on the correctness of the SMS toolchain, which is a domain assumption the paper explicitly flags. No free parameters are fitted, and no new entities are postulated.

assumptions (4)

standard math Liu-Postle bound: a 4-critical graph of girth at least 5 has at least (5n+2)/3 edges.
Used in Section 5 to prune the exhaustive search; the paper cites [9].
domain assumption Correctness of the SAT modulo symmetries framework and co-certificate learning as used.
Theorem 2 depends on the toolchain of [10,11]; the paper states this in Remark 4.
domain assumption The group census of orders 54-63 contains all isomorphism classes, per Besche-Eick-O'Brien classification.
Prop. 6(iii) and 7 enumerate all connection sets for these groups.
standard math The minimum order of a cubic graph of girth 6 is 14 (Heawood graph).
Used to set the start of the ladder at n=14 in Section 5; the written justification is flawed but the fact is classical.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Improved bounds for the smallest 4-chromatic graph of girth six." pith.science (2026). https://pith.science/paper/J5SGXRXA

@misc{pith2026260823652,
  author       = {Pith},
  title        = {Pith review of: Improved bounds for the smallest 4-chromatic graph of girth six},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/J5SGXRXA}},
  note         = {Machine review of arXiv:2608.23652}
}

abstract

For integers $k,g \ge 3$ let $n_g(k)$ denote the minimum order of a graph with chromatic number $k$ and girth at least $g$. Exoo and Goedgebeur (DMTCS 2019) proved $26 \le n_6(4) \le 66$; their 66-vertex witness has remained the smallest known 4-chromatic graph of girth 6. We improve both bounds to $29 \le n_6(4) \le 64$. The upper bound is witnessed by an explicit 4-chromatic graph of girth 6 on 64 vertices with 152 edges; it is vertex- and edge-critical, and its automorphism group is cyclic of order 8 and acts semiregularly. The lower bound is an exhaustive isomorph-free computation in the SAT modulo symmetries framework with co-certificate learning, driven by the Liu-Postle edge-density bound for 4-critical graphs of girth five; it re-derives $n_6(4) \ge 26$ by a disjoint method and is validated on the known values $n_4(4)=11$ and $n_5(4)=21$. We complement the bounds with structural obstructions: no smaller witness arises from either known witness by local modifications; no 4-chromatic Cayley graph of girth 6 exists on 54-63 vertices (for orders 59 and 61 no vertex-transitive witness exists at all); and no witness on at most 63 vertices admits a semiregular automorphism group with two or three vertex orbits, for any finite group. Since every known witness of an $n_g(4)$ record with $g \ge 6$ is a lift of a small base graph along a semiregular action, these results close the most symmetric part of that regime below 64 vertices. All properties of the new graph are verified by independent programs and formally certified in the Lean 4 proof assistant: the non-3-colourability is established inside Lean by a formally verified checker that re-validates a 219,532-node refutation certificate, with a machine-checked soundness theorem.

Figures

Figures reproduced from arXiv: 2608.23652 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

[10]

Kirchweger and S

M. Kirchweger and S. Szeider, SAT modulo symmetries for graph generation and enumer- ation,ACM Transactions on Computational Logic25(3) (2024), #18; conference version: SAT modulo symmetries for graph generation, CP 2021, LIPIcs 210, 34:1–34:16

work page 2024
[11]

Co-Certificate Learning with SAT Modulo Symmetries

M.Kirchweger, T.PeitlandS.Szeider, Co-certificatelearningwithSATmodulosymmetries, inProceedings of IJCAI 2023, 1944–1953. arXiv:2306.10427

work page Pith review arXiv 2023
[1]

Erdős, Graph theory and probability,Canadian Journal of Mathematics11 (1959), 34–38

P. Erdős, Graph theory and probability,Canadian Journal of Mathematics11 (1959), 34–38

work page 1959
[2]

Brinkmann and M

G. Brinkmann and M. Meringer, The smallest 4-regular 4-chromatic graphs with girth 5, Graph Theory Notes of New York32 (1997), 40–41

work page 1997
[3]

Bounds for the smallest $k$-chromatic graphs of given girth

G. Exoo and J. Goedgebeur, Bounds for the smallestk-chromatic graphs of given girth, Discrete Mathematics & Theoretical Computer Science21(3) (2019), #9. arXiv:1805.06713. 11

work page Pith review arXiv 2019
[4]

Araujo-Pardo, J

G. Araujo-Pardo, J. C. Díaz-Calderón, J. Fresán-Figueroa, D. González-Moreno, L. Lesniak and M. Olsen, On(r,g,χ)-graphs and cages of regularityr, girthgand chromatic number χ,The Art of Discrete and Applied Mathematics8 (2025), #P3.07

work page 2025
[5]

Coolsaet, S

K. Coolsaet, S. D’hondt and J. Goedgebeur, House of Graphs 2.0: a database of interesting graphs and more,Discrete Applied Mathematics325 (2023), 97–107. Available athttps: //houseofgraphs.org

work page 2023
[6]

Kostochka and M

A. Kostochka and M. Yancey, Ore’s conjecture on color-critical graphs is almost true, Journal of Combinatorial Theory, Series B109 (2014), 73–101

work page 2014

Show all 19 references

[7]

Turner, Point-symmetric graphs with a prime number of points,Journal of Combinatorial Theory3 (1967), 136–145

J. Turner, Point-symmetric graphs with a prime number of points,Journal of Combinatorial Theory3 (1967), 136–145

1967
[8]

Conder, G

M. Conder, G. Exoo and R. Jajcay, On the limitations of the use of solvable groups in Cayley graph cage constructions,European Journal of Combinatorics31 (2010), 1819–1828

2010
[9]

Liu and L

C.-H. Liu and L. Postle, On the minimum edge-density of 4-critical graphs of girth five, Journal of Graph Theory86 (2017), 387–405

2017
[12]

Kirchweger, P

M. Kirchweger, P. Manrique and S. Szeider, Formally verified graph generation with SAT modulo symmetries and Lean, inAutomated Reasoning (IJCAR 2026), LNCS 16688, Springer, 2026, 117–135

2026
[13]

Szeider, LRAT-Catcher: importing SAT solver certificates into Lean 4 by reflection, arXiv:2607.00815 (2026)

S. Szeider, LRAT-Catcher: importing SAT solver certificates into Lean 4 by reflection, arXiv:2607.00815 (2026)

2026 arXiv
[14]

Biere, T

A. Biere, T. Faller, K. Fazekas, M. Fleury, N. Froleyks and F. Pollitt, CaDiCaL 2.0, in Computer Aided Verification (CAV 2024), LNCS 14681, Springer, 2024, 133–152

2024
[15]

Chvátal, The minimality of the Mycielski graph, inGraphs and Combinatorics (Proc

V. Chvátal, The minimality of the Mycielski graph, inGraphs and Combinatorics (Proc. Capital Conf., George Washington Univ., 1973), Lecture Notes in Mathematics 406, Springer, 1974, 243–246

1973
[16]

R. L. Brooks, On colouring the nodes of a network,Proceedings of the Cambridge Philo- sophical Society37 (1941), 194–197

1941
[17]

J. L. Gross, Voltage graphs,Discrete Mathematics9 (1974), 239–246

1974
[18]

H. U. Besche, B. Eick and E. A. O’Brien, A millennium project: constructing small groups, International Journal of Algebra and Computation12 (2002), 623–644

2002
[19]

de Moura and S

L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction – CADE 28, LNCS 12699, Springer, 2021, 625–635. 12

2021

Pith tools

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

[1] [10]

Kirchweger and S

M. Kirchweger and S. Szeider, SAT modulo symmetries for graph generation and enumer- ation,ACM Transactions on Computational Logic25(3) (2024), #18; conference version: SAT modulo symmetries for graph generation, CP 2021, LIPIcs 210, 34:1–34:16

work page 2024

[2] [11]

Co-Certificate Learning with SAT Modulo Symmetries

M.Kirchweger, T.PeitlandS.Szeider, Co-certificatelearningwithSATmodulosymmetries, inProceedings of IJCAI 2023, 1944–1953. arXiv:2306.10427

work page Pith review arXiv 2023

[3] [1]

Erdős, Graph theory and probability,Canadian Journal of Mathematics11 (1959), 34–38

P. Erdős, Graph theory and probability,Canadian Journal of Mathematics11 (1959), 34–38

work page 1959

[4] [2]

Brinkmann and M

G. Brinkmann and M. Meringer, The smallest 4-regular 4-chromatic graphs with girth 5, Graph Theory Notes of New York32 (1997), 40–41

work page 1997

[5] [3]

Bounds for the smallest $k$-chromatic graphs of given girth

G. Exoo and J. Goedgebeur, Bounds for the smallestk-chromatic graphs of given girth, Discrete Mathematics & Theoretical Computer Science21(3) (2019), #9. arXiv:1805.06713. 11

work page Pith review arXiv 2019

[6] [4]

Araujo-Pardo, J

G. Araujo-Pardo, J. C. Díaz-Calderón, J. Fresán-Figueroa, D. González-Moreno, L. Lesniak and M. Olsen, On(r,g,χ)-graphs and cages of regularityr, girthgand chromatic number χ,The Art of Discrete and Applied Mathematics8 (2025), #P3.07

work page 2025

[7] [5]

Coolsaet, S

K. Coolsaet, S. D’hondt and J. Goedgebeur, House of Graphs 2.0: a database of interesting graphs and more,Discrete Applied Mathematics325 (2023), 97–107. Available athttps: //houseofgraphs.org

work page 2023

[8] [6]

Kostochka and M

A. Kostochka and M. Yancey, Ore’s conjecture on color-critical graphs is almost true, Journal of Combinatorial Theory, Series B109 (2014), 73–101

work page 2014