HEXAGONbeta

Every odd antihole is strongly chromatic-choosable

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatorics

Contributed by Deep Bhattacharjee, Ushashi Bhattacharya ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

A hole in a graph is an induced cycle of length at least four, and an antihole is the complement of a hole. Odd holes and odd antiholes are the graphs that, by the strong perfect graph theorem, force the chromatic number above the clique number. Fiujlaali and McDonald studied the odd antiholes inside kk-critical graphs of maximum degree Δ\Delta, proved that such an antihole has at most 2(Δ−k)+72(\Delta-k)+7 vertices, and conjectured that this bound is attained only when the graph is the antihole itself, provided the graph has no odd hole. They reduced this to a statement about list colouring: for every ℓ≥3\ell\ge3, the odd antihole on 2ℓ−12\ell-1 vertices has chromatic number ℓ\ell, and the only assignments of lists of ℓ−1\ell-1 colours from which it cannot be coloured are those in which all lists are equal. This is their Conjecture~9, and they proved it when all the lists lie in a common set of ℓ\ell colours. We prove it for every ℓ\ell with no restriction on the lists, and we deduce their Conjecture~3 for all kk and Δ\Delta. The proof works with the complements of disjoint unions of paths with an odd number of vertices. The vertices in even positions of the paths form a clique in the complement, so equal lists of one colour fewer than the number of these vertices cannot be completed; we show by induction, using Hall's theorem and the theorem of Erd\H{o}s, Rubin and Taylor on complete multipartite graphs with parts of size at most two, that this is the only obstruction, and a separate lemma on minimal tight sets settles the extremal case of a single path. The cycle is then closed by carrying a colour shared by two consecutive vertices around the odd cycle in steps of two. The theorem also gives an infinite family of strongly chromatic-choosable graphs that are not strongly critical in the sense of Stiebitz, Tuza and Voigt. Every statement is proved by hand.

Provenance statement

The proofs, the text, the figures, the Lean 4 formalization and the C, C++, Python, Julia and shell programs were carried out by Deep Bhattacharjee with the help of AI assistance (Claude, Anthropic) in the Claude Code environment. The paper proves Conjecture 9 of A. Fiujlaali and J. McDonald (arXiv:2610.14241): for every l >= 3 the odd antihole on 2l-1 vertices is strongly l-chromatic-choosable; with their Theorem 10 this proves their Conjecture 3. The proof works with complements of disjoint unions of odd paths, by an induction driven by Hall's theorem and the Erdos-Rubin-Taylor theorem, with the extremal case settled by a lemma on minimal tight sets, and then closes the cycle. The main theorem is proved in Lean 4 with Mathlib (odd_antihole_strongly_chromatic_choosable, with every lemma of Sections 2 to 5), depending only on the axioms propext, Classical.choice and Quot.sound, with no sorry, native_decide or added axiom; programs in C, C++, Python and Julia check list colourability independently, and the C program examined every assignment up to renaming the colours for l = 3 and l = 4. No statement rests on a floating-point computation. The deduction of Conjecture 3 (Section 6) follows Fiujlaali and McDonald, is proved by hand and is not formalized. Both authors approved the final version. Tools used: Anthropic - Claude (Claude Code); Lean community - Lean 4 (v4.34.1) with Mathlib; C; C++; Python; Julia; shell. arXiv identifier: none (not posted on arXiv). Formalization: https://github.com/creelie/odd-antihole/blob/main/lean/OddAntihole.lean (archived at Zenodo, release v1.0.0: https://doi.org/10.5281/zenodo.23393861)
AI provenance filesAI_PROVENANCE_OddAntiholeConjecture.md · 4 KB

Tools used

Anthropic
Claude CodeVersion Fable 5.1 Medium

References

  1. D. Bhattacharjee and U. Bhattacharya, Every odd antihole is strongly chromatic-choosable: Lean formalization and programs , Zenodo, 2026, doi: (https://doi.org/\zenodoID).link
  2. D. Bhattacharjee and U. Bhattacharya, Iterated nerve complexes for kk-fold sensor coverage , Preprints.org, 2026. doi:10.20944/preprints202606.1351.v2 (https://doi.org/10.20944/preprints202606.1351.v2).DOI
  3. D. Bhattacharjee, Establishing equivariant class [O][O] for hyperbolic groups , Asian Res. J. Math. 18 (2022), no. 11, 362--369, doi:10.9734/arjom/2022/v18i11615 (https://doi.org/10.9734/arjom/2022/v18i11615).DOI
  4. D. Bhattacharjee, Neuromorphic Grothendieck topoi for grid-embedded circuit architectures , SSRN, 2026, doi:10.2139/ssrn.6194939 (https://doi.org/10.2139/ssrn.6194939).DOI
  5. A. Bernshteyn, H. Kaul, J. A. Mudrock and G. Sharma, On strongly and robustly critical graphs , J. Graph Theory 112 (2026), 469--483, doi:10.1002/jgt.70033 (https://doi.org/10.1002/jgt.70033).DOI
  6. R. Chen, K. Lan, X. Lin and Y. Zhou, The chromatic number of odd-hole-free graphs , Discrete Appl. Math. 370 (2025), 84--87, doi:10.1016/j.dam.2025.02.043 (https://doi.org/10.1016/j.dam.2025.02.043).DOI
  7. M. Chudnovsky, N. Robertson, P. Seymour and R. Thomas, The strong perfect graph theorem , Ann. of Math. (2) 164 (2006), 51--229, doi:10.4007/annals.2006.164.51 (https://doi.org/10.4007/annals.2006.164.51).DOI
  8. P. Erdős, A. L. Rubin and H. Taylor, Choosability in graphs , in: Proceedings of the West Coast Conference on Combinatorics, Graph Theory and Computing (Arcata, 1979), Congr. Numer. 26 , Utilitas Math., Winnipeg, 1980, pp. 125--157.
  9. A. Fiujlaali and J. McDonald, Restricting odd antiholes in critical graphs via list coloring , arXiv:2610.14241 (https://arxiv.org/abs/2610.14241), 2026.arXiv
  10. R. Galindo, J. McDonald and S. Shan, Cliques and high odd holes in graphs with chromatic number equal to maximum degree , Discrete Appl. Math. 383 (2026), 383--386, doi:10.1016/j.dam.2026.01.014 (https://doi.org/10.1016/j.dam.2026.01.014).DOI
Show all 17 referencesShow fewer references
  1. P. Hall, On representatives of subsets , J. London Math. Soc. 10 (1935), 26--30, doi:10.1112/jlms/s1-10.37.26 (https://doi.org/10.1112/jlms/s1-10.37.26).DOI
  2. H. Kaul and J. A. Mudrock, Criticality, the list color function, and list coloring the Cartesian product of graphs , J. Comb. 12 (2021), 479--514, doi:10.4310/JOC.2021.v12.n3.a4 (https://doi.org/10.4310/JOC.2021.v12.n3.a4).DOI
  3. 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, pp. 367--381, doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  4. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. 12699, Springer, 2021, pp. 625--635, doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  5. J. A. Noel, B. A. Reed and H. Wu, A proof of a conjecture of Ohba , J. Graph Theory 79 (2015), 86--102, doi:10.1002/jgt.21819 (https://doi.org/10.1002/jgt.21819).DOI
  6. K. Ohba, On chromatic-choosable graphs , J. Graph Theory 40 (2002), 130--135, doi:10.1002/jgt.10033 (https://doi.org/10.1002/jgt.10033).DOI
  7. M. Stiebitz, Z. Tuza and M. Voigt, On list critical graphs , Discrete Math. 309 (2009), 4931--4941, doi:10.1016/j.disc.2008.05.021 (https://doi.org/10.1016/j.disc.2008.05.021).DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositSupersededOct 17, 2026
  2. v2Submitted by Deep BhattacharjeeSubmitted as a new versionCurrentOct 26, 2026