Erdős imagined The Book, in which God keeps the perfect proof of every theorem. Mathematicians, he said, need not believe in God — but they must believe in The Book.
This is not The Book. This is the small pile of pages we could get a machine to sign.
Das Buch is a program that attacks open problems in mathematics and files only the results a Lean 4 kernel will certify. No page here rests on human review, on a reviewer's good mood, or on our word. Each one is a file you can recompile yourself.
Don't trust — verify.
In 1976 John Molluzzo asked a question that is easy to state and was not easy to answer.
Take n numbers mod m in a row. Under each neighbouring pair, write their sum mod m.
Repeat until one number is left. You get a triangle — a Steinhaus triangle — with
n(n+1)/2 entries. Call it balanced when every residue 0, 1, …, m−1 appears exactly the
same number of times. For that to be possible at all, m must divide n(n+1)/2.
Molluzzo's question: is that obvious necessary condition also sufficient?
The strong form demands a balanced triangle of every admissible size. It is not a
formality — it is false for some moduli (there is no balanced triangle of size 5 mod 15,
nor of size 6 mod 21). It was known to hold for m = 2, 3, 4, 5, 7 and every odd m.
m = 6 was the smallest case still open. It is now settled — affirmatively.
theorem molluzzo_m6_strong_fin (n : ℕ) (hn : 6 ∣ n * (n + 1) / 2) :
∃ a : Fin n → ZMod 6, ∀ r : ZMod 6, tcountFin n a r = n * (n + 1) / 2 / 6For every n with 6 ∣ n(n+1)/2, there is a first row over ℤ/6ℤ whose Steinhaus triangle
is balanced.
The witness is not an existence argument — it is eight explicit words of period 24, one for
each admissible class of n mod 24. The array such a word generates is doubly 24-periodic: a
wallpaper. The size-n triangle tiles into 24×24 blocks plus two boundary strips, and each
residue is counted exactly, on the tile and on the strips.
| What the kernel signs | |
|---|---|
| Theorem | molluzzo_m6_strong_fin |
| Axioms | {propext, Classical.choice, Quot.sound} — the three standard ones, nothing added |
| Cheats | 0 sorry · 0 native_decide |
| Toolchain | Lean 4 v4.30.0 + Mathlib (pinned commit) |
| Third party | a neutral GitHub runner recompiles it on every push — the green badge above |
📄 Read the page → · 📖 The write-up → · 📕 The paper (PDF) →
Standing on: the framework of periodic first rows is Jonathan Chappelon's, and his 2025
paper (arXiv:2508.05159) settles the weak problem — infinitely
many balanced sizes — for every modulus; for m = 6 it reaches the sparse sizes n = 72λ. The
step from infinitely many sizes to every size is what is added here. Earlier cases are due to
Harborth (m = 2) and Chappelon–Eliahou (m = 4).
📐 Almost-perfect Lee codes of packing radius 2 — the ten open dimensions, closed at the finite level
In 2024 Zhou and Zhou proved that an almost-perfect linear Lee code of packing radius 2 in ℤⁿ
can exist only for n in a list of twelve values, and conjectured that none exists for n ≥ 3
(arXiv:2210.04550, IEEE Trans. Inform. Theory 70(6),
3965–3980). Codes exist for n = 1, 2. The other ten —
n ∈ {11, 29, 47, 56, 67, 79, 104, 121, 134, 191}
— are the whole gap between their theorem and the conjecture, and nobody has closed one since.
The authors note that the smallest, n = 11, is already a constrained search of size ≈ 2⁴⁰,
and that they did not run it.
A finite obstruction is exhibited for all ten, and its finite core is kernel-verified.
theorem no_fiber_n11 : ... = true := by decide
#print axioms no_fiber_n11
-- 'no_fiber_n11' does not depend on any axiomsZero axioms — not the usual three, none. The nine remaining dimensions carry finite-field
certificates and depend on [propext] alone; the thirteen assembled theorems carry the three
standard ones. Neither file imports Mathlib: they are plain
Lean 4 core, so anyone can replay them with a bare toolchain in about a minute.
The mechanism: the two group-ring conditions collapse into the single identity
S² = 4H − S⁽²⁾ + (2n−2)e; since n²+n+1 factors in all ten cases, project onto a cyclic
quotient and transform over a finite field. The spectrum then satisfies
ĉ(2t) = (2n−2) − ĉ(t)², so along each doubling orbit it is an orbit of one quadratic and
its seed must be a periodic point of it. Between 4 and 343 candidates per dimension. None
survives.
The group-ring core is now settled for all ten dimensions, and for every abelian group of each
order — thirteen Lean theorems, 0 sorry, 0 native_decide. With two cited, published
theorems (Xu–Zhou's characterisation and Zhou–Zhou's dimension restriction, neither formalised
here) that settles the conjecture. It stays in margins/ for exactly that reason: the Lee-code
side of the problem is cited, not compiled.
And the method is not ours. Projection onto a cyclic quotient plus a finite-field Fourier
argument is due to Zhang–Zhou (2019) and W. He (2021) — the latter being reference [7] of the
very paper this builds on. He stops at two obstructions he names himself: an algebraic one where
8n−7 is a square, and a computational one he states verbatim ("our computer is not powerful
enough … for v = 37 or any larger prime numbers"). What is added here is crossing both, over all
abelian groups, with a kernel to check it.
📐 Read the margin → · 📖 The write-up →
Nothing to install. Click the green verify badge. That is a machine that is not ours, recompiling the proof from scratch and printing the axioms it depends on.
Ten seconds, zero dependencies — exact integer arithmetic, no Lean:
python3 pages/molluzzo-6/verifie_construction.py 1200
python3 pages/molluzzo-6/strong_vs_weak_demo.py
Checks every admissible size up to 1200, and shows the strong-vs-weak gap explicitly.
Ten minutes, the real thing — in any Mathlib v4.30.0 project (lake exe cache get):
lake env lean CafeMolluzzo6.lean
# expect: molluzzo_m6_strong_fin depends on axioms: [propext, Classical.choice, Quot.sound]
One minute, no Mathlib at all — the Lee-code margin imports nothing, so a bare Lean toolchain is enough:
cd margins/apll-r2
echo "leanprover/lean4:v4.30.0" > lean-toolchain
lean MoonshineFiberN11.lean # expect: does not depend on any axioms
lean MoonshineFp9.lean # expect: nine theorems, axioms [propext]
python3 verify_certificates.py
The file also machine-proves that its own definitions are honest (fidelity_*): that ℤ/6ℤ
really has six elements, that the rule really is the Steinhaus sum, and that the small cases are
balanced non-vacuously. A green build cannot certify that a statement says what you think it
says — so those lemmas pin it down, and the write-up
states the correspondence in plain language.
An entry carries only what the kernel has proven, and its claim is calibrated to its status.
pages/ |
Full results — an unconditional Lean proof of the canonical statement. A page returned to The Book. |
epsilon/ |
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 result that rests on a
hypothesis is conditional, and the condition is named in the theorem itself. A partial result
is a reduction or a note — never a solution.
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; few reach a page. Each survivor passes, in order, through a literature scan, blind and informed solving attempts, exact-arithmetic falsification, an adversarial reader whose only job is to break the proof, Lean formalization, a statement audit, and a hard prior-art re-check on the day of publication.
Full index: INDEX.md · Landing page: dasbuch-catalia.github.io/the-book
- We do not claim to have resolved anything filed under
epsilon/ormargins/. - We do not call a conditional result "resolved" — the condition is always named.
- We do not ask for trust. Every claim above is a file the kernel signs, or it is labelled a reduction, a note, or a conditional result.
Contributions are AI-assisted and machine-verified. How a proof was found has no bearing on whether it is correct; the Lean kernel checks it either way, and so can you. Sponsor: Catalia.
See CITATION.cff, or use the "Cite this repository" button in the sidebar.
Code (*.lean, *.py, CI): MIT. Write-ups and prose: CC-BY 4.0. See LICENSE.
From the Scottish Café to the Lean kernel — the Book files only what the machine will sign.
— DAS BUCH · CATALIA —