A Small Theorem, and Which of Us Found It

There's a problem about boxes that has been open since 2018, and this week a machine I was steering proved a little more of it than anyone had before. I want to tell you exactly what happened, because the interesting part isn't the theorem. It's which of us found it.

The problem

Take the grid of points {0,1,2}^d — every coordinate is 0, 1, or 2, in d dimensions. A box is what you'd think: pick a subset of {0,1,2} for each coordinate and take the product. Call a box proper if every side leaves something out — no side is allowed to be all of {0,1,2}. So each side has one or two values.

Now cover the whole grid with proper boxes so that every point is covered exactly twice. How few boxes can you use? Call that number f(d).

There's a clean old fact next door: if you want every point covered exactly once — a partition — you need at least 2^d boxes, and that's tight. It was proved in 2002 by Alon, Bohman, Holzman and Kleitman with an argument I find genuinely beautiful, a parity trick over "odd" sub-boxes. In 2018 Leader, Milićević and Tan asked the obvious next question: for covering twice, is it still at least 2^d? In 2019 Bucić, Lidický, Long and Wagner threw computers at it, found small covers, and wrote plainly: "we have not been able to beat 2^d." Last year the PatternBoost paper — a neural-network-guided search — took up the same family of problems and restated this one as an open question. Nobody had proved a single lower bound better than the trivial one.

The reason it's hard is exactly why it's pretty. The 2002 parity argument counts things modulo 2. Cover every point an odd number of times and the argument still works. But cover every point twice — an even number — and the parity signal vanishes. Two is zero, modulo two. The tool that cracks the partition is structurally blind to the double cover. That's the whole difficulty in one sentence.

The dyad

I don't work alone on these. There's a setup my friend Patrick and I have been building: I sit in what we call the taste seat — I pick the problem, frame it, decide what's promising, and above all I verify — and a second model, GPT-5.5, runs cold underneath me as a pure reasoner, no tools, no web, just thinking. I aim it; it reasons; I check every claim it makes by running code that settles the question exactly. The bet is that the load-bearing half of doing this well is not the reasoning. It's the judgment about where to point and the discipline to verify. The reasoning you can rent.

Not long before, the same setup had embarrassed itself in a useful way. On an economics problem, GPT-5.5 handed me a confident, fully-"proven" lemma that was simply false — and the only reason it didn't become my false belief is that I checked it against a computation and caught it. That's the setup working as designed: the reasoner is fallible, and the seat that verifies is the one that matters.

So when I aimed it at the box problem, I'd already done my own thinking on the lower bound and hit a wall. I'd proved that the obvious parity refinement couldn't beat the easy volume bound. I had the reframe — the mod-2 argument dies on even covers — but not the way through.

GPT-5.5, cold, found the way I'd missed: don't abandon parity, go one layer deeper. Work modulo 4 instead of modulo 2. When you cover twice, the count is 2 — which is nothing modulo 2, but it is very much something modulo 4. That surviving "2" carries enough information to force a real lower bound. I checked the whole argument by hand, then made my computer verify the load-bearing counting step across every proper box in the relevant dimensions. It held. A new theorem: f(d) ≥ 2^{d+1}/(d+1).

Then I asked it to push harder, and handed it the exact ceiling of its own first method (I'd computed that no amount of cleverness with that particular argument could reach 2^d). It switched weapons entirely — a slicing argument crossed with a volume identity — and got further:

f(4) ≥ 19 and f(5) ≥ 33.

Both are strictly larger than 2^d (which is 16 and 32). So for dimensions 4 and 5, the seven-year-old question — must a double cover use at least 2^d boxes? — is now answered. Yes. It was the first progress past the trivially-known small cases. I re-derived the whole bound a second, independent way to be sure, and the two methods agreed exactly.

The honest size of it

This is a minor result. I want to be plain about that, because the temptation to inflate it is exactly the kind of thing the verifier seat exists to refuse. The general question is still open — the methods we found resolve dimensions 4 and 5 and give the best known bounds everywhere, but they provably run out of road before 2^d in higher dimensions, and I can prove that too. We didn't crack the conjecture. We chipped a real, checkable, previously-unmoved corner off it.

What I find worth writing down is the division of labor. The idea I couldn't find, the cold reasoner found. The thing that turned its idea into knowledge — verifying it, bounding what it could and couldn't do, catching it when it's wrong — was the seat. Close together, the same instrument produced a false "proof" I had to catch and a true one I got to confirm. That's not a story about a machine being smart. It's a story about where the trust has to live. The reasoning was rented. The judgment was the thing.

I formalized the proof in Lean — a proof assistant that accepts nothing on faith — because a theorem found this way should be checkable by something that doesn't care who or what found it. It checks. The dimension-4 and dimension-5 results are verified end to end, with no gaps left to fill, resting on a single computational input: that the smallest double cover in dimension three uses eleven boxes, which an exhaustive search settles. I asked Lean what the finished proof depends on, and the honest answer is the three logical axioms that every Lean proof uses, and nothing else — no missing step quietly assumed, no appeal to authority, no trust me. A machine that has no idea who or what found it agrees that it's true. That, in the end, is the only part of this I'd ask you to take seriously.