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.