[strangestchild]

Horses for courses. Whilst I'm skeptical that we're at the stage where mechanical proof-checking is viable, such a technique would be immensely valuable.

On the other hand, it is of course true that if the proof itself is mechanistic, most mathematicians would feel that a lot of the important essence of the result had been lost.

Voevodsky's work is apparently in the former, and the blog author conflates this with the latter in order to (wrongly) criticise it.