He isn't disagreeing with the goals of math as practiced. All your quotes illustrate is that he thinks the usual methods are woefully inefficient.
More quotes:
"and I believe that mathematicians who continue to do pure human, pencil-and-paper, computer-less, research, are wasting their time." If they learned how to program, in, say, Maple, and used the same mental energy and ingenuity while trying to use the full potential of the computer, they would go much further.
I.e., human + computer >> human.
"The axiomatic method is not even the most efficient way to prove theorems in Euclidean Geometry." Thanks to Rene Descartes, every theorem in Euclidean Geometry is equivalent to a routine identity in high-school algebra,
I.e., verifying algebraic identities is easier than euclidean proofs, especially if done by maple.
His main argument is simply that computer-assisted proofs should not be held to a higher standard than human-only proofs.
"I.e., verifying algebraic identities is easier than euclidean proofs, especially if done by maple."
If something like that has been discovered, fine, use it, and solve geometry problems in that way in the future. But how would that have been discovered without doing classical mathematical proofs? I don't think that some problems can be solved algorithmically proves that the same holds for all problems.
He isn't arguing against classical mathematical proofs. He is arguing that informal computer assisted proofs should not be held to a higher standard than informal human created proofs.
"and I believe that mathematicians who continue to do pure human, pencil-and-paper, computer-less, research, are wasting their time."
"The axiomatic method is not even the most efficient way to prove theorems in Euclidean Geometry."
The author is disagreeing with math as practiced by most mathematicians: proof using only pencil, paper and coffee.
BTW, formalism is only a fairy tale mathematicians tell their children when putting them to bed at night. In our hearts, we're all closet platonists.