lean

Three axioms and one disclosed seam

Four verification tools, one certificate: every machine-checked theorem mechanically reduced to three classical axioms with zero unfinished proofs — and the one place two provers cannot talk to each other, named right in the theorem statements.