HEXAGONbeta

Three-colour cuboids 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 2 / Nov 04, 2026 / CC BY 4.0

Abstract

We determine the least number of four-colour cubes that guarantees a cuboid with monochromatic faces using exactly three colours. Each source uses all four colours of a fixed palette; only proper rotations are allowed, and interior faces need not match. For integer side lengths 2≤a≤b≤c2\le a\le b\le c, the sharp threshold for the corner-and-edge frame is max⁡{16a−3,4(a+b+c)−16,⌊(24c−1)/5⌋}\max\{16a-3,4(a+b+c)-16,\lfloor(24c-1)/5\rfloor\}, and the complete-cuboid threshold is max⁡{abc,16a−3,⌊(24c−1)/5⌋}\max\{abc,16a-3,\lfloor(24c-1)/5\rfloor\}. The three frame bounds arise from colour-bucket capacity, the number of positions and balanced checkerboards. The upper bound combines corner containment, a weighted graph selecting edge directions, and Hall's theorem. For cubic frames the threshold is 16n−316n-3, with exactly two failing collections of size 16n−416n-4. For n≥3n\ge3 we classify every failure of size at least 14n14n and count these collections and the inclusion-maximal ones. The case n=2n=2 answers the threshold question in Problem 2 of Berkove, Eickemeyer and Schulman (2018). All threshold, stability and counting results are formalised in Lean.

Provenance statement

GPT-6-Astra (OpenAI), used through Codex under the author's direction, developed the original argument, computational searches, Lean formalisation and manuscript, including the v2 extension from cubes to cuboids. Claude Opus 5.5 (Anthropic), used through Claude Code, contributed the minority-cube counting argument, the edge-count balance proof, simplifications, figures, review, and the comparator statements for stability, near-extremal classification and restricted targets. The Lean library proves all threshold, stability and counting results. A standalone challenge that imports only mathlib restates 58 statements, including the cuboid thresholds and their corollaries. The challenge is checked with the Lean comparator and replayed through the Lean, nanoda and con-ron kernels. The only axioms are propext, Classical.choice and Quot.sound; there is no sorry and no native_decide. No human expert has independently reviewed the work. Detailed attribution is in the repository's formalization.yaml. Changes since v1: sharp frame and complete-cuboid thresholds for all side lengths 2 ≤ a ≤ b ≤ c; the stability and counting results added to the comparator challenge (35 → 58 statements); revised exposition.

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. v1 · 12 pagesSubmitted by Jason DaviesInitial depositSupersededNov 03, 2026
  2. v2 · 16 pagesSubmitted by Jason DaviesSubmitted as a new versionCurrentNov 08, 2026