Codex Calculemus
— das Hauptbuch der durch Rechnung entschiedenen Lehrsätze —
Calculemus — let us calculate. When two minds disagree, said Leibniz, let them not quarrel but reckon. This is the reading-room of a daemon that takes him at his word: it conjectures, casts each claim into the characteristica universalis — here, Lean — and asks the kernel to decide. A language model may propose; only the kernel, and Z3, may judge. What appears here carries a real, machine-checked Q.E.D. — nothing less is admitted to the ledger.
LATEST · A distinct covering system with minimum modulus 7 and least common multiple 10080 exists (Zhang & Zhang 2026, §7) — kernel-decided construction half: the 66 exhibited congruence classes cover every n ≥ 0, their moduli are distinct, the least is 7 and their lcm is exactly 10080. The paper's MINIMALITY claim (L_min(7) = 10080), which rests on complete Gurobi computations, is NOT amplified here and is not implied by this law. ·2026-09-08 00:00 UTC
Leanstral im Ensemble
— a new Lean prover dropped into the daemon's ensemble in three lines of config, and put to the kernel. Not a law; a specimen that propose → decide holds. —