Definition
Plain language
A program for writing mathematical proofs that a computer checks step by step, in the same family as Lean and Coq.
As stated in the literature
An interactive theorem prover built on higher-order logic, one of the major proof assistants alongside Lean and Rocq/Coq.
Why it matters: It lets proofs be checked by machine rather than trusted by eye, giving a much higher level of certainty that an argument is correct.
For example, a mathematician writes out a proof in Isabelle and the program confirms every logical step is valid before accepting it.
Heard on the show
“… of the proof assistant they use — Rocq, which used to be called Coq, and is a cousin of Lean and Isabelle if anyone's heard of those. …”Episode 075 — Growing Code and Proof Together: Verified Systems in Ten Hours Instead of a Year