Das Räderwerk

Everything in Die Gesetze is the kernel's verdict. This page is the apparatus — written plainly, in our voice — that explains how a conjecture becomes a kernel-checked law, and why no language model is ever trusted to decide one.

The charter

Leibniz dreamed of a characteristica universalis — a formal language in which any dispute could be settled not by rhetoric but by reckoning: calculemus. The daemon that bears his name builds a sliver of that dream, around a single inversion of the usual order: the model proposes; mechanical checkers decide. Language models are powerful but unsound — they will argue for a false claim as fluently as a true one. So they are confined to proposal roles: surveying, conjecturing, formalizing, drafting proofs. The verdict belongs only to instruments that cannot be charmed — the Lean kernel and the Z3 solver.

The six stages

A cycle runs six stages in order. SURVEY draws live edges of a domain (and cross-domain analogies) as seeds. CONJECTURE has a model propose a claim. FORMALIZE autoformalizes it into a Lean statement and runs the cheap gates first — Z3 cheap refutation, then structural novelty against a corpus of known results, then faithfulness (an adversarial gaming-witness search). Only a claim that is plausibly true, genuinely novel, and faithful to its statement is allowed to cost any proof compute. DERIVE and DEMONSTRATE draft and check a proof: an ensemble of provers proposes tactic scripts, and the kernel must verify N+1 independent proofs before consensus is reached. PROMULGATE admits the law to the Codex — only on a real kernel Q.E.D.

The trust tiers

Every decision edge is tagged with the tier of evidence behind it. Mechanical — the kernel and Z3 — is the only tier that may promote a law. Adversarial — the gaming-witness that tries to satisfy a statement while violating its claim — guards faithfulness. Judged — a model's opinion — is admitted only for claims that resist operationalization, and even then it is budget-bounded and never sufficient on its own. The trust policy is checked at promotion, so no cycle can promulgate a law whose proof the kernel did not certify.

Why mechanical

A kernel-valid proof of a mis-stated theorem is worse than no proof — it is most authoritative exactly when it is most wrong, and the ledger makes it permanent. That is why the gate is built before the firehose: the cheap, mechanical checks run before any expensive proof, and the one irreducible residual — does the formal statement faithfully capture the human claim? — is attacked adversarially and bounded, never waved through by a judge. The slowness and the refusals are the design. The character of the ledger is as much what it forbids as what it admits.