HEXAGONbeta

R(12,12) ≥ 1661 by extending the Mathon–Shearer coloring

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatorics

Contributed by Yue Ma ↗

Version 1 / Nov 10, 2026 / CC BY 4.0

Abstract

We prove that R(12,12)≥1661R(12,12)\ge 1661 by constructing a red/blue coloring of the edges of K1660K_{1660} with no monochromatic K12K_{12}. We start from a classical (11,11)(11,11)-coloring on 1596 vertices, delete 21 of its vertices and add 85 new ones. Toward the remaining 1575 vertices, each new vertex has either the same colors as one of the deleted vertices or a single color. The deleted vertices include two pairs whose members have complementary colors toward every other vertex, and these pairs weaken the conditions that the new vertices must satisfy. The proof reduces to a finite check on the new vertices and is formally verified in Lean 4.

Author comments: 11 pages. The coloring, the check programs, the outputs of two exhaustive searches and the Lean 4 proof are at https://github.com/YueMa0/r1212-1661, archived as version 1.0.1 at https://doi.org/10.5281/zenodo.24087657.

Provenance statement

The work was carried out with the AI system Claude (Anthropic, model Claude Opus 5.5), used through the coding agent Claude Code. The author directed the project, chose its directions and approved each stage. Claude designed and ran the searches (a SAT-based search with CaDiCaL called through PySAT, and a local search written for this project), wrote the check programs and the Lean 4 proof, ran the exhaustive searches and the kernel checks, and drafted the paper, which the author revised over several rounds of annotations. The work continues the earlier release r1212-1658, which started from exploratory work by GPT-6 Astra (OpenAI). The correctness of the result does not rely on the AI system: the Lean proof is checked by the Lean kernel and by the independent kernel nanoda, and two exhaustive searches by separate programs confirm that the coloring has no monochromatic K_12. The programs, data and logs of these checks are at https://github.com/YueMa0/r1212-1661.

Tools used

Anthropic
Claude OpusVersion Claude Opus 5.5
Lean
LeanVersion 4.32.1
OpenAI
CodexVersion GPT-6 Astra

References

  1. CaDiCaL SAT solver, https://github.com/arminbiere/cadical.link
  2. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction -- CADE 28 , Lecture Notes in Computer Science 12699, Springer, 2021, 625--635.
  3. lean4export: plain-text declaration export for Lean 4, https://github.com/leanprover/lean4export.link
  4. Y. Ma, R(12,12)≥1642R(12,12)\ge1642: a colouring of K1641K_{1641}, a Lean proof and computer checks, software repository, 2026, https://github.com/YueMa0/r1212-1642, archived at https://doi.org/10.5281/zenodo.23770924.DOI
  5. Y. Ma, R(12,12)≥1658R(12,12)\ge1658: a colouring of K1657K_{1657}, a Lean proof and computer checks, software repository, 2026, https://github.com/YueMa0/r1212-1658, archived at https://doi.org/10.5281/zenodo.23827702.DOI
  6. Y. Ma, R(12,12)≥1661R(12,12)\ge1661: a colouring of K1660K_{1660}, a Lean proof and computer checks, software repository, 2026, https://github.com/YueMa0/r1212-1661, archived at https://doi.org/10.5281/zenodo.23963534.DOI
  7. R. Mathon, Lower bounds for Ramsey numbers and association schemes, J. Combin. Theory Ser. B 42 (1987), 122--127.
  8. The mathlib Community, The Lean mathematical library, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , ACM, 2020, 367--381.
  9. nanoda_lib: a type checker for Lean 4, https://github.com/ammkrn/nanoda_lib.link
  10. PySAT: a toolkit for SAT-based prototyping in Python, https://github.com/pysathq/pysat.link
Show all 16 referencesShow fewer references
  1. S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin. , Dynamic Survey DS1, revision 18, April 24, 2026.
  2. J. B. Shearer, Lower bounds for small diagonal Ramsey numbers, J. Combin. Theory Ser. A 42 (1986), 302--304.
  3. M. Tatarevic, On the Ramsey number R(12,12)R(12,12), research note, February 14, 2017, https://mtatar.wordpress.com/2017/02/14/r12/.link
  4. M. Tatarevic, A constructive two-parameter Ramsey increment, arXiv:2608.06531 (https://arxiv.org/abs/2608.06531), 2026.arXiv
  5. M. Tatarevic, Ramsey increment theorem: Lean formalization, executable construction, and graph certificates, software repository, 2026, https://github.com/milostatarevic/ramsey-increment-theorem.link
  6. X. Xu, Z. Shao and S. P. Radziszowski, More constructive lower bounds on classical Ramsey numbers, SIAM J. Discrete Math. 25 (2011), 394--400.

Version history

  1. v1 · 11 pagesSubmitted by Yue Ma11 pages. The coloring, the check programs, the outputs of two exhaustive searches and the Lean 4 proof are at https://github.com/YueMa0/r1212-1661, archived as version 1.0.1 at https://doi.org/10.5281/zenodo.24087657.CurrentNov 09, 2026