Definition
Plain language
Software that checks a mathematical proof step by step and accepts it only if every step is logically valid.
As stated in the literature
An interactive theorem-proving system such as Lean, Rocq, or Coq, built around a small trusted kernel that mechanically verifies that each step of a formalized proof follows from its logical rules.
Also called: proof assistants
Why it matters: It removes human error from checking proofs, giving a level of certainty that hand-checking can't match.
For example, a mathematician can feed a proof into one of these and trust the result only after the software confirms every single step is valid.
Heard on the show
“… And the equivalent of that on-site inspector, in this paper, is a feature of the proof assistant they use — Rocq, which used to be called Coq, and is a cousin of Lean and Isabelle if anyone's …”Episode 075 — Growing Code and Proof Together: Verified Systems in Ten Hours Instead of a Year