Interactive Theorem Prover: the class of programming languages (Lean, Coq, Isabelle) that guarantee the correctness of mathematical statements written in them by requiring machine-checkable proofs
