The Grundy domination number is not multiplicative on strong products

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

Contributed by Deep Bhattacharjee ↗

Version 1 / Oct 23, 2026 / CC BY 4.0

Abstract

The strong product of the octahedron with a graph HH on 2121 vertices of Grundy domination number 1010 has Grundy domination number at least 2121. This disproves the conjecture of Bre\v{s}ar, Bujt\'as, Gologranc, Klav\v{z}ar, Ko\v{s}mrlj, Patk\'os, Tuza and Vizer that $\ggr(G\sprod H)=\ggr(G)\ggr(H)$ for all graphs GG and HH.

Provenance statement

Deep Bhattacharjee chose the problem and directed the work. Claude (Anthropic), through Claude Code, carried out the searches and computations, wrote the checking programs and the Lean 4 proofs and drafted the paper. Refutes Conjecture 22 of Brešar et al. The proofs are written out in the paper; the programs and their outputs are in the release. The author approved the final version. Code and data: release v1.0.0, https://github.com/creelie/grundy-strong-product/releases/tag/v1.0.0.

Tools used

Anthropic
Claude CodeVersion Opus 5.5 Ultracode

References

  1. D. Bhattacharjee, The Grundy domination number is not multiplicative on strong products: Lean 4 development, programs and data , version 1.0.0, Zenodo, 2026. 10.5281/zenodo.23378021; https://github.com/creelie/grundy-strong-productDOI
  2. K. Bell, K. Driscoll, E. Krop and K. Wolff, Grundy domination of forests and the strong product conjecture , Electron. J. Combin. 28 (2) (2021), #P2.12. 10.37236/9507DOI
  3. B. Brešar, Cs. Bujtás, T. Gologranc, S. Klavžar, G. Košmrlj, B. Patkós, Zs. Tuza and M. Vizer, Dominating sequences in grid-like and toroidal graphs , Electron. J. Combin. 23 (4) (2016), #P4.34. 10.37236/6269DOI
  4. B. Brešar, T. Gologranc, M. Milanič, D. F. Rall and R. Rizzi, Dominating sequences in graphs , Discrete Math. 336 (2014), 22--36. 10.1016/j.disc.2014.07.016DOI
  5. R. Herrman and S. G. Z. Smith, A proof of the Grundy domination strong product conjecture , arXiv:2212.04565, 2022 (withdrawn). https://arxiv.org/abs/2212.04565arXiv
  6. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci., Springer, Cham, 2021, pp. 625--635. 10.1007/978-3-030-79876-5_37DOI

Version history

  1. v1Submitted by Deep BhattacharjeeInitial depositCurrentOct 23, 2026