I think this isn’t true? Comparator verifies proofs; it’s not clear to me what it even means to mechanically verify a statement to be valid. The statement is manifestly valid anyway - it’s hard to find much simpler statements of maths, slightly odd facts of mathlib’s natural arithmetic like the saturating behaviour of natural subtraction notwithstanding.