HEXAGONbeta

Sharp thresholds for five-colour cube assemblies

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

Contributed by Jason Davies ↗

Version 1 / Nov 10, 2026 / CC BY 4.0

Abstract

We determine the least pool sizes guaranteeing a frame or a complete a×b×ca\times b\times c box from unit cubes whose faces use all five colours of a fixed palette, for every a,b,c≥2a,b,c\ge2. Proper rotations are allowed; the target has monochromatic exterior faces using all five colours. The frame threshold is max⁡{15,4(a+b+c)−16,2(a+b+c)+1}\max\{15,4(a+b+c)-16,2(a+b+c)+1\}, and the complete-box threshold is max⁡{abc,15,2(a+b+c)+1}\max\{abc,15,2(a+b+c)+1\}. The proof combines a certified fifteen-cube corner theorem with elementary Hall arguments and a uniform three-variety obstruction. It completes the five-colour frame column left open by Berkove, Eickemeyer and Schulman (2018). All threshold statements are formalised in Lean. A fixed-size flow formulation decides feasibility and constructs assemblies in time linear in the explicit source list. We also determine the corner thresholds when the number of source varieties is bounded, and classify all fourteen-cube obstructions into 56 classes under common colour relabelling and simultaneous reflection, described by three structural forms. The minimum size of a collection capable of reproducing every 2×2×22\times2\times2 target is also fifteen.

Provenance statement

GPT-6-Astra (OpenAI), used through Codex, developed the arguments, computational search, verification programs, Lean formalisation and manuscript under the author's direction. Claude Opus 5.5 (Anthropic), used through Claude Code, contributed illustrations, the migration to the shared colour-cubes-core library, and review and editing of the manuscript. The author initiated and directed the research and takes responsibility for the content. Results are formalised in Lean 4 with mathlib; a standalone Mathlib-only comparator challenge of sixteen claims was accepted by Lean's kernel and NanoDa. Axioms: propext, Classical.choice, Quot.sound; no sorry or native_decide. Detailed attribution and verification scope are in the repository's formalization.yaml.

Tools used

Anthropic
Claude CodeVersion 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. E. Berkove, A. Eickemeyer and M. Schulman, The 4-Color Cubes Puzzle , Integers 18 (2018), A68. doi: 10.5281/zenodo.10680216 (https://doi.org/10.5281/zenodo.10680216). Journal PDF (https://math.colgate.edu/~integers/s68/s68.pdf).DOI
  3. P. Hall, On Representatives of Subsets , Journal of the London Mathematical Society s1-10 (1) (1935), 26--30. doi: 10.1112/jlms/s1-10.37.26 (https://doi.org/10.1112/jlms/s1-10.37.26).DOI
  4. J. Edmonds and R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems , Journal of the ACM 19 (2) (1972), 248--264. doi: 10.1145/321694.321699 (https://doi.org/10.1145/321694.321699).DOI
  5. J. Davies, Three-colour solutions from four-colour cubes , hexagon: 2611.00070v1 (https://hexagonmath.org/2611.00070v1) (2026). Accompanying repository (https://github.com/jasondavies/four-to-three-colour-cubes).hexagon
  6. J. Davies, colour- cubes- core : palette-independent Lean definitions and proofs for face-coloured cubes, Lean library (2026). Release v1.0.0 (https://github.com/jasondavies/colour-cubes-core/tree/v1.0.0), https://github.com/jasondavies/colour-cubes-core.link
  7. 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
  8. The mathlib Community, The Lean Mathematical Library , in Proceedings of 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. v1 · 34 pagesSubmitted by Jason DaviesInitial depositCurrentNov 09, 2026