Software that verifies mathematical proofs are logically correct, acting as a checker for formal mathematics.