Comment by margorczynski

Verify the statement is correct + it doesn't introduce any new axioms + doesn't use "sorry" etc.

Order of magnitudes easier than verifying the whole thing by hand and gives a much better guarantee of correctness