Ah, but the nice thing about constructing formal proofs is you can immediately tell if the output is correct.

Yes, but you also need to make sure the input is correct! For example, your idea of automatically formalising a paper needs to somehow make sure that the result means the same as the paper.

I don't blindly believe everything it says. I've caught it making mistakes plenty of times. But there's simply no going back anymore. There's no replacing what it can do and the kind of workflow it offers.