Evidence
What machine-checked means
The definition behind the theorem count: what qualifies as proven, which provers check it, how the proofs are stress-tested, and where the boundary of the guarantee sits.
What counts as proven
A theorem counts as machine-checked only when a proof assistant accepts it end-to-end. Complete theorems are mechanized independently in both Lean 4 and Isabelle/HOL with zero local axioms. Axiom-backed theorems are machine-checked modulo explicitly declared local axioms — named real-analysis backbones, each documented and tracked for discharge. Nothing in between is counted as proven.
Provers & checkers
Lean 4 v4.30.0 with Mathlib and Isabelle2025-2 with AFP 2026-06-01, both pinned by digest in container images. Runtime numerical checking uses an SMT portfolio: Z3 4.16.0, CVC5 1.3.4, Yices2 2.6.5, dReal 4.21.06.2.
Methodology
Zero sorry placeholders across the corpus. Headline theorems must check in both provers independently; a negative-control suite of deliberately false variants must fail to compile; proof mutation testing and catalog-conformance gates run in CI on every change.
The trust boundary
The proofs are over exact real arithmetic: they cover the mathematical model, not the compiled floating-point implementation — that bridge is checked numerically at runtime, and closing it formally is open, tracked work. Framework assumptions (Lipschitz continuity, compact sets, bounded disturbance, hardware isolation) are declared inputs, not theorems.
Artifacts & verification
The theorem catalog and the runtime conformance registry are kept consistent by a CI census gate; tagged releases ship with a SHA-256 checksum manifest.