Building Peano Lab#
A little Lean for Peano arithmetic — and a guided tour of how such systems are built.
Peano Lab is a lightweight, readable theorem prover for Peano arithmetic. It runs entirely in the browser next to the Lambda Lab, but its central lesson is not a flashy tactic: every QED is checked again by an independent kernel against the original theorem. Tactics may search, guess and fail. The kernel sees only an explicit proof certificate.
This part tells the construction story from the implementation diary. Read it in order:
Why Peano arithmetic develops the staged path from computation to induction and first-order logic.
The kernel and the De Bruijn criterion explains the trusted boundary, proof terms, capture-safe substitution and the audit that made independent checking non-negotiable.
Anatomy of a tactic follows one tactic from a goal transformation to a certificate with proof-wide metavariable substitution and transactional failure.
Tacticals: when tactics become a language builds sequencing, choice, repetition, focusing and their rollback laws.
Induction and the theorem ladder climbs from the defining equations to a checked zero-product proof.
Checked arithmetic automation separates numerical computation, polynomial normalization, and bounded search from the certificates that justify their results.
compact_arith: searching for a small PA certificate follows one theorem from a 30,030-node generic elaboration to a 180-node checked record, then designs a bounded equality tactic without confusing a best-found certificate with a proven minimum.
The deliberate limits draws the line around PA, Gödel’s theorems, bounded search, and the facilities that a production prover such as Lean adds.
Training a Peano policy without trusting it turns the prover into a warm headless data and evaluation service, then develops replay-validated synthetic data, leakage-safe prompts and splits, completion-only SFT, kernel-judged search, and a reproducible Helios protocol without placing a learned model inside the trusted base.
The working design lives in
docs/PEANO_LAB_DESIGN.md,
the task board in
PLAN/09_peano_lab.md.
Then use Checked tutorials to replay a premise-free hand proof of addition
commutativity, a source-level symm_all tactical walkthrough, and a numerical-normalization proof.
Every pa> block and browser deep link in this part is replayed through the real driver during the
book gate; prose examples do not get a private, easier semantics.
The full library is executable too. The checked theorem ladder follows the original 23 scripted entries through order totality and the zero-product core capstone, then a public 26-entry modular-arithmetic extension to the fourth-power modulo-five capstone. It also links to the separately validated M20 foundational snapshot. The chapter explains how theorem reuse is packaged as self-contained Cuts whose complete branches are checked by the reviewed kernel rule, without granting theorem names or hashes any authority. It also links each statement to the browser and Lean 4 cross-checking surface. M9 then turns the same checked interactions into a reproducible proof-trace corpus and fixes a kernel-judged evaluation protocol for later small-model experiments; at that milestone no model was trained. The dated implementation diary preserves the design choices, bugs and objections behind the polished account.
M19 is the authorized continuation of that deliberately frozen M9 protocol. The policy-training chapter explains the compact headless adapter and the small-model experiment. Its first attested release contains 2,522 independently kernel-checked roots and exactly 10,000 next-tactic rows, split by genealogy, canonical formula, and exact policy prompt and reproduced byte-for-byte from raw traces. The first WMI Qwen3-1.7B pilot completed, scoring 0/4 at pass@4 on the frozen induction/order benchmark and 1/8 on one fresh direct-witness probe. The chapter treats this as a curriculum diagnosis, not broad proving ability.
M11 extends that core with three ordinary checked entries—one_mul, mul_one, and add_mul—to
complete the commutative-semiring basis for certificate-producing arithmetic normalization. M12’s
argument-free ring turns that basis into checked polynomial identities; the ladder chapter gives
the complete odd-square induction proof and makes its explicit trans/rewrite boundary visible.
M13 adds bounded norm_num for closed numerical islands and arithmetic-aware hints. The new
arithmetic-automation chapter contrasts its exact equality contract with simp, ring, and auto,
and records why general PA, nonlinear hypothesis solving, and Presburger omega remain outside it.
M14 then treats browser delivery as another explicit boundary: versioned caching, negotiated WASM
compression, and concurrent source transfer reduce cold network cost without changing one proof rule.
The limits chapter distinguishes that runtime boot from theorem proving. M15 adds a replayable
current-branch artifact: active text remains unchecked, while only a successful kernel QED may
produce the retained script’s final qed. The tactics and ladder chapters explain why downloading
that program is still separate from checking a certificate or admitting a library theorem. M17
applies the same distinction to multiline paste: a bounded complete script runs sequentially
through the ordinary session owner, and its final qed gains no new authority.
M18 applies it once more to certificate size. The compact_arith tactic searches a fixed
PA recurrence-template space for a small proof of one rigid equality, optionally using an explicit
ordered list of equality hypotheses. It neither chooses an outer induction invariant nor invents an
existential witness, and its cost report is never a substitute for independent checking.
M20 begins a general foundational arithmetic library. Its first independently validated branch snapshot extended the
original 23-entry base to 51 checked entries. That snapshot and the 49-entry public-catalog source
remain provenance: fourteen post-core records coincide, so their initial reconciliation contained
63 unique entries rather than their arithmetic sum. Subsequent native passes extend the current
local candidate to 384 checked theorems: the 23-entry base, 212
post-baseline foundational entries, twelve further unique modular capstones,
and 137 quadratic-residue-campaign entries. The checked route now includes division and
remainder, relational gcd, balanced-natural Bézout, Gauss cancellation, the general prime-divisor
characterization, Euclid’s lemma, constructive equality/divisibility/primality decisions, bounded
nontrivial-factor search, proper-factor descent, prime-divisor existence,
balanced-congruence transitivity and addition/multiplication,
both directions between bounded congruence and a remainder decomposition,
functional single-position Gödel-β decoding equivalent to bounded congruence,
constructive binary CRT, and a one-code/two-position β client under an explicit
modulus-coprimality premise. It now also proves beta-modulus coprimality under
the explicit conditions \(j=i+\mathit{gap}\) and \(\mathit{gap}\mid c\), applies
that result to the two-position client, and constructs a nonzero common
multiple of every positive natural through a given bound. The newest seven
certificates turn that resource into bounded-prefix pairwise beta-modulus
coprimality, prove both multiplicative orientations of coprimality, descend a
balanced congruence from a product modulus to each divisor modulus, and check
one generic binary_crt_fold_step that preserves every old congruence modulo
a divisor of the accumulated product while adding a new modulus. Unconditional
beta-modulus coprimality is false: with \(c=1\), the family contains moduli
\(3\) and \(6\). Six further certificates now extend the accumulated beta-modulus
product, extend congruences for values decoded from an already supplied code,
combine those successor steps, and use ordinary induction to construct the
four-part prefix invariant through every \(k\le N\). The projected theorem
bounded_beta_crt_for_existing_code is deliberately not a recoding theorem:
because its residues already come from \(b\), extensionally \(z=b\) is already a
solution. Later checked layers supply genuine finite-prefix recoding, exact
β-coded prefix-product traces, greatest-prime-divisor descent, canonical
factorization existence, and extensional uniqueness. Their native FTA
conjunction checks at 73,767 nodes/depth 99 with 2,184 self-contained Cuts and
no DNE. The associated 385-node research catalog records those 384 checked
entries alongside no planned theorem and one representation-blocked
conventional integer-coefficient Bézout interface. prime_unbounded is now a
checked constructive client of bounded common multiples and prime-divisor
existence.
The arithmetic part now has a guided zero-to-FTA route and a generated
384-proof theorem atlas that links
every exact statement and authored script backward to prerequisites and
forward to direct clients.
This is local candidate authority; it does not claim that every new theorem
card has already been promoted to the production browser.