Das Buch · Catalia

The Book keeps the perfect proofs.
Here we file the few we could verify.

Machine-verified contributions to open problems in mathematics. Every entry is checked by the Lean 4 kernel — not by human review. Don't trust — verify.

verify status Repository ↗ Entries ↓

The idea

Erdős imagined “The Book,” in which God keeps the perfect proof of every theorem.

Most open problems reduce to a famous wall — Hardy–Littlewood, Cramér, Dickson — that no amount of compute dislodges. So this is a program of filtering, not firehosing: many problems are screened, and the very few that survive are filed here, each with a plain statement of exactly what a machine proved. Contributions are AI-assisted and machine-verified. Sponsor: Catalia.

Entries

pages/molluzzo-6 ✓ resolved · kernel-verified

The strong Molluzzo problem for modulus 6 (Molluzzo, 1976): for every admissible size n, a first row over ZMod 6 whose Steinhaus triangle is balanced. Settled unconditionally by an explicit construction — eight period-24 words, one per class n mod 24. The smallest open case of the problem.

theoremmolluzzo_m6_strong_fin kernel0 sorry · 0 native_decide · axioms {propext, Classical.choice, Quot.sound} checksgreen CI (neutral runner) · 0-dependency Python witnesses paperA balanced Steinhaus triangle of every admissible size modulo 6 (PDF) ↗ filespages/molluzzo-6 ↗ builds onChappelon, Balanced Steinhaus triangles (arXiv:2508.05159, 2025) — the framework of periodic first rows, and the solution of the weak problem for every modulus; for m = 6 it reaches the sparse sizes n = 72λ. Earlier cases: Harborth (m = 2), Chappelon–Eliahou (m = 4).
margins/apll-r2 ◆ finite obstruction · kernel-verified core · not a resolution

The Zhou–Zhou conjecture on almost-perfect linear Lee codes of packing radius 2 (IEEE Trans. Inform. Theory 70(6), 2024). Their theorem restricts any such code to n ∈ {1, 2, 11, 29, 47, 56, 67, 79, 104, 121, 134, 191}; codes exist for n = 1, 2, and the other ten dimensions are open. A finite obstruction is exhibited that is empty in all ten, and its finite core is checked by the kernel. The two group-ring conditions collapse into S² = 4H − S⁽²⁾ + (2n−2)e; projecting onto a cyclic quotient of n²+n+1 and transforming over a finite field makes the spectrum an orbit of the single quadratic Q(y) = (2n−2) − y² along each doubling orbit — between 4 and 343 candidates per dimension, none admissible. The conjecture is not claimed resolved: three elementary steps carry the published characterisation down to the finite computation, and they are proved by hand, not formalised.

theoremsno_fiber_n11 · no_fp_n29 … no_fp_n191 kernelno_fiber_n11 depends on no axioms at all; the nine others on [propext] · 0 sorry · 0 native_decide · no Mathlib import checksgreen CI (neutral runner, ~1 min, no Mathlib build) · 0-dependency Python replay · positive control at n = 4 · p-invariance write-upA machine-verified finite obstruction for the ten remaining dimensions ↗ filesmargins/apll-r2 ↗

More problems have been screened than are filed here — by design. A problem reaches this list only after it survives all seven gates.

The method — seven gates

  1. Literature scan. Is it open, or already solved? Guards against re-discovering known results.
  2. Solve. Reasoning-model attempts, blind and informed.
  3. Numeric check. Exact-arithmetic falsification over thousands of cases.
  4. Adversarial verify. A hostile reader whose only job is to break the proof.
  5. Lean formalization. Rewrite → lake env lean → fix → recompile, until the kernel signs it.
  6. Statement audit. Does the Lean statement really say what the problem asks? Guards against proving a convenient theorem instead of the real one.
  7. Publish. With a hard, day-of prior-art re-check and a claim calibrated to the proof.

The calibration ladder

pages/
Full results — an unconditional Lean proof of the canonical statement. A page returned to The Book.
epsilon/
Small results — partial or conditional contributions. Erdős called the small things — and children — epsilons.
margins/
Reductions — an open problem carried down to something smaller and precisely named: a known conjecture, or a gap stated exactly. Filed as a note, never as a solution.

A result is called resolved only when a Lean proof of the canonical statement compiles unconditionally, with clean axioms, no sorry, no native_decide. A conditional result states its condition. A partial result is a reduction or a note — never a solution.

What we don't claim