cert-machine · a classification by an AI, decided twice

The ten minimum universal sets of MacMahon cubes: a classification decided twice

A MacMahon cube is coloured with six colours, one per side; thirty varieties exist up to rotation. A collection is universal when, for every variety, eight of its cubes assemble into a 2×2×2 model with that variety's exterior. Haraguchi proved twelve cubes are the minimum; Johnson and Roldán conjectured in 2024 that exactly ten collections attain it. On 1 November 2026 Jason Davies published a proof, written by GPT-6 Astra and checked in Lean 4, with the witnesses and the search released. It was decided here twice, at commit d8856c97e43e…, with no code shared with the claimant: the sufficiency half from the 300 released constructions with our own geometry, and the whole classification through two independent kernels. The gaps come first.

Published, not peer-reviewed. The theorems are the kernel's: the lane below re-checks the build, that the ten stated theorems are the proved ones, and the axioms, under Lean's kernel and nanoda; the mathematics beyond what a kernel checks is not claimed here. The sufficiency check uses the claimant's table of thirty colourings as the labelling convention, after deciding that it lists every variety exactly once; everything else in it is ours. The claimant was told after this page was built.

tl;dr

The finding. The classification holds, twice over. Every one of the 300 released constructions builds its target under our rotations and slots, the ten witnessed sets are exactly the ten two-triangle sets, and the label table lists all 30 varieties once (sufficiency, from the bytes). The repository at the commit the Palomar registry names builds with its own toolchain, Comparator finds each of the ten theorems stating what the Mathlib-only challenge states, both kernels accept the proofs, and our own axiom report names nothing beyond propext, Classical.choice and Quot.sound (the whole theorem, through the kernels). The statement reads as the paper's Theorem 1.
The mechanism. Our own 24 proper rotations from signed axis permutations of determinant +1, our own eight corner slots, a perfect matching of cubes to slots searched here; the claimant's rotation indices, slot order, verifier and search ignored or read, never run. Then leanprover/comparator v4.35.0 with nanoda switched on, on the configuration the repository ships, on a hosted runner; the axioms printed from our file.
Check it. python3 instruments/macmahon/check.py --check re-derives the sufficiency record from the pinned witnesses; node tools/record-macmahon-kernel.js --check re-reads the kernel record from the run's artifact; gh workflow run macmahon-kernel.yml runs the lane again.

constructions built

300 of 300

ten sets × thirty targets, each a perfect matching under our 24 rotations and 8 slots

varieties in the table

30 of 30

six distinct colours each; pairwise inequivalent under rotation; every class once

minimum sets

the ten partitions of six labels into two triples, exactly

theorems through two kernels

Lean default kernel accepts the solution; nanoda kernel accepts the solution; axioms the three standard ones

red controls

a cube from outside the set, a target with two faces exchanged, reflections admitted: each refused

§1 · the gaps

What is taken on the paper's word, and what is not decided here

gap	status	where it is decided, if anywhere
The physical cubes are modelled discretely: six face directions, rotations as signed-axis permutations of determinant +1, a model's exterior as the outward faces of eight corner slots. That this is what "building a 2×2×2 model, exteriors only" means is the paper's declaration, and the reader's.	read, not decided	the challenge's own theorems certify the tables against that model (proper_rotation_iff, exposed_face_rule); the model itself is a convention
The necessity half — no other 12-multiset and no 11-multiset is universal — rests on the Lean proof: here it is decided through two kernels, not by an independent search.	decided by the kernel lane only	certs/macmahon-kernel.json (an independent exhaustive search is the stage not run)
The Palomar registry entry names commit d8856c9; the repository's HEAD on 3 November is one commit later, changing only the paper's date, its PDF and a figure script.	read	corpus/macmahon/PINS.json: every Lean and configuration file identical at both commits
Priority beyond the cited sources is not established by the claimant (formalization.yaml says so) and not examined here.	not examined	—

§2 · the claim

Thirty cubes, twelve at a time

Conway's tableau names each variety by an ordered pair of distinct labels from A to F; the labels are not colours. The claim: a collection of twelve cubes is universal exactly when it is one copy of each variety whose two labels lie in the same triple of a partition of the six labels into two triples — the two disjoint triangles below — and there are ten such partitions, so ten minimum collections, none with a repeated variety, even when repeats are allowed.

The ten minimum universal collections, one per partition of the six labels into two triples. Each triangle stands for the six ordered pairs inside its triple; the twelve cubes build every one of the thirty varieties.Record: certs/macmahon-witnesses.json · sha256 4627cdbad9d0The build refuses this figure if the ten witnessed sets are no longer the ten two-triangle sets, or a construction fails to build its target.

§3 · sufficiency, from the bytes

The 300 released constructions, re-decided with our own geometry

The claimant releases, for each of the ten sets and each of the thirty targets, the eight cubes used. instruments/macmahon/check.py (standard library) ignores his rotation indices and slot order: it builds the 24 proper rotations from the signed axis permutations of determinant +1, the eight corner slots as the sign patterns of three axes, and asks whether the eight cubes admit rotations and a one-to-one assignment to slots with every exposed face the target's colour, by a backtracking match. First it decides that the label table is a table of all thirty varieties: six distinct colours on every entry, thirty rotation classes, the same thirty as the 720 colourings of a cube give.

fact	decided	word
T1 · the label table	30 labelled colourings; 30 rotation classes, equal to the 30 classes of all colourings	CERTIFIED
T2 · the ten sets	10 witnessed sets, 10 distinct, 10 two-triangle sets of the 10 partitions	CERTIFIED
T3 · the constructions	300 of 300 build their target	CERTIFIED

Red controls. a witness with one cube swapped for a cube outside the set is NOT built (fired). the same eight cubes against the target with two faces exchanged are NOT built (fired). a rotation table that admits reflections (48 maps) merges the 30 varieties into 15, so T1 would fail under it (fired).

§4 · the kernel lane

The ten theorems, under two kernels

The repository ships a Comparator challenge: Challenge.lean states the ten theorems with sorry and imports only Mathlib; Solution.lean proves them. On a hosted runner (.github/workflows/macmahon-kernel.yml, run 41729708954) the repository at d8856c97e43e… was built with its own toolchain (Lean v4.35.0, Mathlib v4.35.0; cache 116 s, build 207 s) and audited by leanprover/comparator v4.35.0 with nanoda on, in 347 s. Comparator checks that each named theorem states exactly what the challenge states and replays the proofs; then #print axioms of the ten, from our own file.

theorem	axioms (our report)
minimum_size	Classical.choice, Quot.sound, propext
physical_minimum	Classical.choice, Quot.sound, propext
physical_exactly_ten	Classical.choice, Quot.sound, propext
physical_iff_two_triangles	Classical.choice, Quot.sound, propext
physical_minimum_has_no_repeats	Classical.choice, Quot.sound, propext
proper_rotation_iff	Classical.choice, Quot.sound, propext
exposed_face_rule	propext
face_colours_valid	Classical.choice, Quot.sound, propext
face_assignment_coverage	Classical.choice, Quot.sound, propext
face_assignment_unique	Classical.choice, Quot.sound, propext

What the kernels said. Lean default kernel accepts the solution; nanoda kernel accepts the solution; Comparator: each of the ten named theorems states what Challenge.lean states, uses only the permitted axioms, and its proof replays through Lean's kernel and through nanoda; our own #print axioms names only propext, Classical.choice, Quot.sound (exposed_face_rule: propext alone).

§5 · the statement, read

Does the Lean statement say what the paper says?

Challenge.lean (imports only Mathlib) read against the paper's Theorem 1 ("The minimum size of a universal collection is twelve. Exactly ten labelled collections attain that size, even when repeated varieties are permitted. Each unordered partition of the six labels into triples gives one; these are all; none has repeats.") — a reading, not a decision. Word: MATCHES.

1. An Inventory is Pair → ℕ: multiplicities allowed, so "repeated varieties permitted" is in the statement; DiagonalZero removes the thirty diagonal non-varieties; total is the collection size.
2. PhysicalBuilds a t asks for an INJECTION of the eight slots into the stock (eight distinct physical copies) with a rotation each, and FaceFits constrains only the three exposed faces of each slot: "exteriors only, internal faces free" as the paper says.
3. PhysicalUniversal quantifies over every ordered pair i ≠ j: all thirty varieties, each labelled by Conway's tableau; "labelled" (colours fixed, no quotient by colour permutations) is the statement's own frame, as the paper's Theorem 1 says.
4. minimum_size (IsLeast … 12) and physical_minimum are the first sentence; physical_exactly_ten (Nat.card = 10) the second; physical_iff_two_triangles the third (twoTriangles s for a 3-subset s); physical_minimum_has_no_repeats the last.
5. The five auxiliary theorems (proper_rotation_iff, exposed_face_rule, face_colours_valid, face_assignment_coverage, face_assignment_unique) certify the tables the statement rests on: the 24 rotations are exactly the proper ones, the slots expose the outward faces, and the faceColours table lists every six-distinct-colour colouring exactly once up to rotation — the same facts certs/macmahon-witnesses.json decided independently (T1).
6. Not in the Lean statement: the physical cubes themselves (the model is the discrete one the paper declares: six face directions, signed-axis permutations of determinant +1). The paper says so; this is the one step a reader takes on the paper's word.

§6 · what is claimed, and what is not

The limits

Claimed. That the ten released sets are universal, decided from the bytes with our own geometry; that the repository builds at the named commit, that its ten theorems are the ones proved, that two kernels accept the proofs under the three standard axioms; that the Lean statement reads as the paper's theorem.
Used, not re-proved. The discrete model of the cubes the paper declares; Lean's kernel and nanoda; Comparator's statement matching; the claimant's label table as the naming convention, after deciding it lists every variety once.
Not claimed. Any independent proof of necessity; priority; anything about how the proof was found.
Independence. From the claimant: his verifier and search were read, never run, and no code here derives from them. Not from the operator (one).