Kolophon
Codex Calculemus is a reading-room for the ledger of an autonomous theorem daemon, Leibniz. The daemon surveys a frontier, conjectures, formalizes each claim into Lean, and — where the claim survives the cheap gates — asks the kernel to calculate whether it holds. This site renders the laws that survived. It is read-only, and it rebuilds whenever a new law is published.
The one rule
An LLM may propose; only a mechanical checker may decide. Conjecture and formalization are drafted by language models, but no model's opinion ever promotes a law. A proof is admitted only when the Lean kernel verifies it. Refutation and the faithfulness gaming-witness are settled by Z3; novelty is settled by structural comparison against a corpus of known results — all mechanical. The one irreducible residual is faithfulness for claims that resist operationalization (open-form): it is attacked adversarially first and only then falls back to a budget-bounded judged review — never silently waved through, and never enough on its own to promote a law. The certificate Q.E.D. is stamped if and only if the kernel verified the proof — it is never hand-set. Everything in Die Gesetze carries one.
What is gathered here
- 3 published laws — Die Gesetze (3 marked specimen — see below).
- 1 circadian cycle of work — Das Tagewerk.
Promotion is not publication
When the kernel verifies a law, the daemon promulgates it to the Codex. It does not publish it. Publication to this public ledger is a separate, deliberate act by a human operator — the daemon can never perform it. So a verified law may sit in the Codex, held back, until someone chooses to open it.
No promulgated laws are currently held back.
On the specimens
Some entries are marked specimen. These are not novel discoveries — they are well-known results, kernel-checked here to show the format of a published law while the daemon's discovery frontier matures. A specimen is honest about being one; it is never counted as a find. The novelty corpus would catch any attempt to pass a textbook result off as new.
On the look of the page
This is the Characteristica surface — Leibniz's, not Leonardo's. Where the sibling Codex Vitruvianus reads as a Renaissance sketchbook in warm vellum and rubric red, this codex is a German Baroque copperplate: a cool laid-paper ground (Tag and Nacht), iron-gall ink, antique-gold illumination and a verdigris-green hand. The marginalia are devices from Leibniz's own world — the dyadic table of De Progressione Dyadica, the I Ching hexagrams he read as binary, the integral ſumma, the monad, the stepped reckoner — drawn in SVG, not photographed. The type is the shared codex hand: Instrument Serif for titles, Instrument Sans for the body, JetBrains Mono for the characteristica.