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.

A note on what is here so far. Every law currently published is a specimen — a well-known result, genuinely kernel-checked, shown only to demonstrate the format while the daemon's discovery frontier matures. None is a daemon discovery yet. See the colophon.