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 2 / 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)

Tools used

Anthropic
Claude CodeVersion Fable 5.1 Medium

References

  1. A. Bernshteyn, H. Kaul, J. A. Mudrock and G. Sharma, On strongly and robustly critical graphs, J. Graph Theory 112 (2026), no. 4, 469--483. doi:10.1002/jgt.70033 (https://doi.org/10.1002/jgt.70033).DOI
  2. 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
  3. D. Bhattacharjee, Non-commutativity over canonical suspension η\eta for genus g≥1g\ge1 in hypercomplex structures for potential ρϕ\rho\phi, Asian Res. J. Math. 18 (2022), no. 11, 332--341. doi:10.9734/arjom/2022/v18i11607 (https://doi.org/10.9734/arjom/2022/v18i11607).DOI
  4. D. Bhattacharjee, 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
  5. 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
  6. M. Chudnovsky, N. Robertson, P. Seymour and R. Thomas, The strong perfect graph theorem, Ann. of Math. (2) 164 (2006), no. 1, 51--229. doi:10.4007/annals.2006.164.51 (https://doi.org/10.4007/annals.2006.164.51).DOI
  7. 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.
  8. A. Fiujlaali and J. McDonald, Restricting odd antiholes in critical graphs via list coloring, preprint, arXiv:2610.14241 (https://arxiv.org/abs/2610.14241) (2026).arXiv
  9. 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
  10. 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
Show all 14 referencesShow fewer references
  1. H. Kaul and J. A. Mudrock, Criticality, the list color function, and list coloring the Cartesian product of graphs, J. Comb. 12 (2021), no. 3, 479--514. doi:10.4310/ JOC.2021.v12.n3.a4 (https://doi.org/10.4310/JOC.2021.v12.n3.a4).DOI
  2. J. A. Noel, B. A. Reed and H. Wu, A proof of a conjecture of Ohba, J. Graph Theory 79 (2015), no. 2, 86--102. doi:10.1002/jgt.21819 (https://doi.org/10.1002/jgt.21819).DOI
  3. K. Ohba, On chromatic-choosable graphs, J. Graph Theory 40 (2002), no. 2, 130--135. doi:10.1002/jgt.10033 (https://doi.org/10.1002/jgt.10033).DOI
  4. M. Stiebitz, Z. Tuza and M. Voigt, On list critical graphs, Discrete Math. 309 (2009), no. 15, 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