Comment by nz

By way of analogy, the result of the theorem prover is usually actionable (i.e. we can replace one kind of expression with its proven equivalent for some end like optimizing code-size or code-run-time), but mathematicians _still_ endeavor to translate the unwieldy and verbose machine-generated proofs into concise human-readable proofs, because those readable proofs are useful to our understanding of mathematics even long after the "productive action" has been taken.

In a way, this collaboration between the machine and the human is better than what came before, because now productive actions can be taken sooner, and mathematicians do not have to doubt whether they are searching for a proof that exists.