HEXAGONbeta

A graph with three card types and five vertex orbits

A mix of human-written and AI-generated textHuman understanding: some partsmath.CO — Combinatoricsmath.GR — Group Theory

Contributed by Deep Bhattacharjee ↗, Ushashi Bhattacharya ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

We prove that the answer to part~(b) of Problem~20.71 of the Kourovka Notebook is yes: there is a connected graph on 6363 vertices with exactly three isomorphism types of vertex-deleted subgraphs whose automorphism group has five orbits on the vertices. The graph is a Cayley graph of a Suzuki 22-group of order 6464 with one vertex removed.

Provenance statement

The construction of the graph, the proofs, the text, the figures, the Lean 4 formalization and the Python, Julia, C, C++ and shell programs were carried out by Deep Bhattacharjee with the help of AI assistance (Claude, Anthropic) in the Claude Code environment. The graph is the Cayley graph of the Suzuki 2-group of order 64 with the identity removed; it is a divisible design graph in the sense of Haemers, Kharaghani and Meulenberg, and its five orbits are separated by a Fano plane carried by the cosets of the centre. The theorem is proved in Lean 4 with Mathlib (K2071.main_theorem and K2071.kourovka_20_71b), depending only on the axioms propext, Classical.choice and Quot.sound, with no sorry, native_decide or added axiom; the finite checks are made by the kernel, and four programs in exact integer arithmetic recompute the graph, its orbits and its card types. No statement rests on a floating-point computation. Part (a) of Problem 20.71 (k = 2) is not treated and stays open; part (c) was answered earlier by J. Prajapati. Both authors approved the final version. Tools used: Anthropic - Claude (Claude Code); Lean community - Lean 4 (v4.34.1) with Mathlib; Python; Julia; C; C++; shell. arXiv identifier: none (not posted on arXiv). Formalization: https://github.com/creelie/urban-chainsaw/blob/main/lean/Kourovka2071.lean (archived at Zenodo, release v2.0.0: https://doi.org/10.5281/zenodo.23384197)
AI provenance filesAI_PROVENANCE_Kourovka2071b.md · 3 KB

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. Unsolved problems in group theory. T he K ourovka notebook, no. 21, version 48 (2026). arXiv:1401.0300 (http://arxiv.org/abs/1401.0300), doi:10.48550/arXiv.1401.0300 (https://doi.org/10.48550/arXiv.1401.0300).arXivDOI
  2. J. Prajapati, A graph with four card types and five vertex orbits: the k=4k=4 case of K ourovka N otebook P roblem 20.71, Preprint, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/10/kourovka-20-71-prajapati.pdf; code at https://github.com/infinityscroll/kourovka-20-71 (2026).link
  3. G. Higman, Suzuki 22-groups, Illinois J. Math. 7 (1963) 79--96. doi:10.1215/ijm/1255637483 (https://doi.org/10.1215/ijm/1255637483).DOI
  4. W. H. Haemers, H. Kharaghani, M. A. Meulenberg, Divisible design graphs, J. Combin. Theory Ser. A 118 (3) (2011) 978--992. doi:10.1016/j.jcta.2010.10.003 (https://doi.org/10.1016/j.jcta.2010.10.003).DOI
  5. D. Bhattacharjee, U. Bhattacharya, S. Bhattacharya, The sphere packing problem in dimension 4, Preprints.org (2026). doi:10.20944/preprints202606.0856.v11 (https://doi.org/10.20944/preprints202606.0856.v11).DOI
  6. D. Bhattacharjee, Establishing equivariant class [O][O] for hyperbolic groups, Asian Res. J. Math. 18 (11) (2022) 362--369. doi:10.9734/arjom/2022/v18i11615 (https://doi.org/10.9734/arjom/2022/v18i11615).DOI
  7. 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
  8. L. de Moura, S. Ullrich, The L ean 4 theorem prover and programming language, in: Automated Deduction -- CADE 28, Vol. 12699 of Lecture Notes in Comput. Sci., Springer, Cham, 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
  9. The mathlib Community , The L ean mathematical library, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, New York, 2020, pp. 367--381. doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 17, 2026