HEXAGONbeta

The ten minimum universal sets of MacMahon cubes

Primarily AI-generated textHuman understanding: some partsmath.CO — Combinatoricscs.DM — Discrete Mathematicscs.LO — Logic in Computer Science

Contributed by Jason Davies ↗

Version 1 / Nov 02, 2026 / CC BY 4.0

Abstract

A collection of six-coloured MacMahon cubes is universal if eight of its cubes can be selected to build a 2×2×22\times2\times2 model of any target variety, with matching exterior colours and no internal matching requirement. We prove that exactly ten labelled collections attain the known minimum size of twelve, even when repeated varieties are allowed, resolving the conjectures of Johnson and Roldán. Usable-cube inequalities force a symmetric multiplicity matrix with row and column sums two; corner coverage then forces two disjoint triangles in Conway's tableau. The written proof is elementary and requires no exhaustive search. The classification and its discrete geometric interpretation are formalised in Lean 4. Exhaustive computation provides a separate check and additional target-count distributions.

Provenance statement

The human author initiated the investigation and directed the AI systems throughout, but wrote no part of the manuscript or of the Lean code. GPT-6-Astra (OpenAI), used through Codex, developed the classification proof and computational investigation, wrote the Lean 4 formalisation, and wrote and revised the manuscript. Claude Opus 5.5 (Anthropic), used through Claude Code, contributed to paper review. The minimum, the classification and their discrete geometric interpretation are formalised in Lean 4 with mathlib, using only the standard axioms propext, Classical.choice and Quot.sound; the proofs and the ten compared statements are checked by Lean's kernel and the independent kernels NanoDa and con-ron. The target-count enumerations are computational and are not formalised. These automated checks are not independent human peer review. The author takes responsibility for the content. Full details are in the paper's section "Declaration of AI-generated research and review".

Formalizations

Tools used

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

References

  1. P. A. MacMahon, New Mathematical Pastimes , Cambridge University Press (1921). Digitised edition (https://archive.org/details/newmathematicalp00macmuoft).link
  2. I. Johnson and É. Roldán, Solution Numbers for Eight Blocks to Madness Puzzle , arXiv:2407.13208v1 (https://arxiv.org/abs/2407.13208v1) (2024).arXiv
  3. K. Haraguchi, On a generalization of ``Eight Blocks to Madness'' puzzle , Discrete Mathematics 339 (4) (2016), 1400--1409. doi: 10.1016/j.disc.2015.12.014 (https://doi.org/10.1016/j.disc.2015.12.014). Preprint arXiv:1408.3696v2 (https://arxiv.org/abs/1408.3696v2); numbered results cited here follow this version.arXivDOI
  4. E. Berkove, D. Cervantes Nava, D. Condon and R. Katz, Automorphisms of S6S_6 and the color cubes puzzle , Australasian Journal of Combinatorics 68 (1) (2017), 71--93. Publisher PDF (https://ajc.maths.uq.edu.au/pdf/68/ajc_v68_p071.pdf). arXiv:1503.07184 (https://arxiv.org/abs/1503.07184).arXiv
  5. E. Berkove, J. Van Sickle, B. Hummon and J. Kogut, An analysis of the (colored cubes)3^3 puzzle , Discrete Mathematics 308 (7) (2008), 1033--1045. doi: 10.1016/j.disc.2007.03.058 (https://doi.org/10.1016/j.disc.2007.03.058).DOI
  6. L. de Moura and S. Ullrich, The Lean 4 Theorem Prover and Programming Language , in Automated Deduction---CADE 28, LNCS 12699 , Springer (2021), 625--635. doi: 10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  7. 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. doi: 10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824). arXiv:1910.09336 (https://arxiv.org/abs/1910.09336).arXivDOI

Version history

  1. v1Submitted by Jason DaviesInitial depositCurrentNov 01, 2026