2

I mean, do ATP's spot some obvious errors in computations or proofs? And if I'm not sure about the correctness of some modern proof found in some article, say for example Mochizuki's proof of the ABC conjecture, can I verify the correctness of the proof by some ATP in reasonable time?

beginnermathematician
  • 21
  • 1
    Converting a traditional proof into a format that an automatic theorem prover can use is a lot of work. – lhf Sep 22 '14 at 11:10

0 Answers0