I think their point is more on the fact that just proving something is only half the work. Intermediate results and proofs are often also of immense value. Right now the output is sloppy proofs and LEAN code. This is useful, but a large part of the effort still lies ahead. And if you are a mathematician you'd rather be working on hard problems than fixing slop.