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.
Assumptions vs. local axioms
Both words appear in the definition above, and a reader who meets them in one paragraph will reasonably take them for one thing. They are not, and the difference decides which of them is debt. They are also not a split of one number: local axioms are what separate complete theorems from axiom-backed ones, while the assumptions sit underneath both.
Assumptions the theorems are stated under
Lipschitz continuity, compact sets, bounded disturbance, hardware isolation and their siblings are hypotheses — declared once in a single registry and cited by the theorems that use them. They apply at every proof status, the complete theorems included: a complete proof is one that introduces no axiom of its own, not one that needs no assumptions. These are not debt. The work is to state them and keep them honest, not to remove them.
Local axioms inside the proofs
An axiom-backed proof declares, as a named axiom, a result it does not derive — general mathematics the prover libraries do not yet formalize: real-analysis and measure-theoretic backbones, textbook results rather than claims about our system. A proof may instead carry a result established elsewhere in the corpus that it does not yet build on. Either way it is debt: each is documented and tracked for discharge, and carrying even one is exactly what keeps a theorem out of the complete count.
Physical premises carried as hypotheses
Where a proof mechanizes a theorem's mathematical shell but a physical fact the framework cannot prove — a hardware, floating-point or reconfiguration premise — is carried as an explicit named hypothesis, the implication is machine-checked and the theorem is still not counted as proven. Those results sit outside both figures published on this site.
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.