> The cost is that the justification for the steps might become opaque to humans. If the machine can tell "this proof is correct". Does the proof really need t

> The cost is that the justification for the steps might become opaque to humans. If the machine can tell "this proof is correct". Does the proof really need to be reviewed by humans? As long the human can easily read the problem which is proved, if the machine says the proof is complete, it should be good enough.