3 ms·

Quis custodiet ipsos custodes?

• Animats 4mo ago
  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 4mo ago
    But don't you still have to logically connect the validity of the proof to desirability of the output?