HEXAGONbeta

Three-colour solutions from four-colour 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 04, 2026 / CC BY 4.0

Abstract

For every n≥2n\ge2, any 16n−316n-3 cubes, each using all four colours of a fixed palette, contain an n×n×nn\times n\times n frame whose exterior faces are monochromatic in exactly three colours; this bound is sharp. For a fixed palette, exactly two collections of 16n−416n-4 cubes fail, and reflection exchanges them. For n≥3n\ge3, every failure of size at least 14n14n lies in one ordinary orientation class with four bounded colour buckets. This gives 2(d+1515)2\binom{d+15}{15} failures at size 16n−4−d16n-4-d, for 0≤d≤2n−40\le d\le2n-4, of which 2(d+1111)2\binom{d+11}{11} are inclusion-maximal. The threshold for a complete cube is max⁡{n3,16n−3}\max\{n^3,16n-3\}; in particular, any n3n^3 source cubes suffice when n≥4n\ge4. The case n=2n=2 answers the threshold question in Problem 2 of Berkove, Eickemeyer and Schulman (2018). The proof combines their corner-containment reduction with orientation constraints and double counting.

Provenance statement

GPT-6-Astra (OpenAI), used through Codex, developed the original research argument, computational search, Lean formalisation and manuscript under the author's direction. Claude Opus 5.5 (Anthropic), used through Claude Code, contributed the minority-cube argument, the balance proof, further simplifications, illustrations and review. The core results (35 statements) are restated in a standalone comparator challenge importing only mathlib, and replayed through the Lean, NanoDa and con-ron kernels; the stability and counting theorems are proved in the library but not yet in that challenge. Axioms: propext, Classical.choice, Quot.sound; no sorry or native_decide. Detailed attribution is 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. E. Berkove, A. Eickemeyer and M. Schulman, The 4-Color Cubes Puzzle , Integers 18 (2018), A68. Journal PDF (https://math.colgate.edu/~integers/s68/s68.pdf).link
  2. 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
  3. 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
  4. 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

Version history

  1. v1Submitted by Jason DaviesInitial depositCurrentNov 03, 2026