I think his point is more subtle than that. Informal paper math doesn't always neatly line up with formal, computer-processed math---such as numerical processi

I think his point is more subtle than that. Informal paper math doesn't always neatly line up with formal, computer-processed math---such as numerical processing or theorem proving. This disconnect can be extremely frustrating: I want to believe paper proofs, but simply writing down the theorem statement in a rigorous way can require significant changes. It's the frustration of understanding something on the surface but then realizing that in fact it makes no sense.