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 · For non-negative integers, the product of max and min recovers a·b, and the difference of their squares factors as (max − min)(a + b) ·2026-07-23 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. —