It’s impressive tech, but giving a false-but-believable proof is substantially worse than saying “I don’t know how to do that”. If it had come back with “I don’t know how to give a proof of Fermat’s Last Theorem in Isabelle”, I wouldn’t have been unimpressed; there are plenty of very cool things it can do. I just think that it being confidently incorrect is a bad thing.

EDIT:

I should point out, it also was wrong with substantially simpler proofs, like the proof of infinite primes.