Eh... A decent compiler will cause a proof to grind to a halt on a typo. I don't really see the difference honestly, besides quantitative complexity. A compute

Eh... A decent compiler will cause a proof to grind to a halt on a typo. I don't really see the difference honestly, besides quantitative complexity. A computer run exhaustive proof is less brittle than a manual exhaustive proof. I think complexity of the proof is just a function of the length. And for a computer proof, that length includes the toolchain.