AI 中文总结
本文将围长为6的最小4-色图的阶数界改进为29≤n₆(4)≤64，构造出64顶点的见证图并通过形式化验证，同时给出结构障碍结果。
AI 中文摘要
对于整数k,g≥3，令n_g(k)表示色数为k且围长至少为g的图的最小阶数。Exoo和Goedgebeur（DMTCS 2019）证明了26≤n₆(4)≤66，他们构造的66顶点图是目前已知最小的围长为6的4-色图。本文将这两个界均改进为29≤n₆(4)≤64。上界由一个明确的64顶点、152条边的围长为6的4-色图作为见证；该图是顶点临界和边临界的，其自同构群为阶8的循环群，且作用半正则。下界是在带共证书学习的SAT modulo symmetries框架下，基于Liu-Postle关于围长为5的4-临界图的边密度界进行的穷尽无同构计算；该方法通过不同途径重新推导了n₆(4)≥26，并通过已知值n₄(4)=11和n₅(4)=21得到验证。我们还通过结构障碍补充了这些界：对任一已知见证图进行局部修改都无法得到更小的见证图；在54至63顶点范围内，不存在围长为6的4-色Cayley图（其中59和61顶点的图完全不存在顶点传递见证图）；且对于任意有限群，最多63顶点的见证图都不允许具有两个或三个顶点轨道的半正则自同构群。由于所有已知的n_g(4)记录见证图（g≥6）都是小基图沿半正则作用的提升，这些结果封闭了该领域中64顶点以下最具对称性的部分。新图的所有性质均通过独立程序验证，并在Lean 4证明助手中形式化证明：非3-可着色性由Lean内部的形式化验证检查器建立，该检查器重新验证了一个219532节点的反驳证书，具有机器检查的正确性定理。
英文摘要
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.
Comments12 pages, 1 figure. Ancillary files: independent verification scripts, SAT certificates, and a self-contained Lean 4 formal proof. Code and data: https://github.com/glaucorampone/G64, archived at doi:10.5281/zenodo.21861488
