[Animats]

The proof checker.

You verify a proof system by having it produce a proof trace:

- Step 3185: Apply rule that a * b = b * a to "length * width" in the current formula.

Then you run a proof trace checker which applies each transformation in sequence and checks that the expected result is obtained.

Provers are complicated, but proof trace checkers are really dumb.

[zahlman]

But don't you still have to logically connect the validity of the proof to desirability of the output?