Harris versus Buzzard

Michael Harris has a new article at quanta. The piece is (uncharacteristically?) coy, referring to the laments of two logicians without divulging either their names or their precise objections, making oblique references to a cabal of 10 mathematicians meeting at the institute, and making no reference at all to his own significant contribution to the subject. But that aside, the piece relates to one of themes from Michael’s book, namely, what is mathematics to mathematicians? In this case, the point is made that mathematics is decidedly not — as it is often portrayed — merely a formal exercise of deducing consequences of the axioms by modus tollens and modus ponens. More controversial, perhaps, is the question of what number theorists stand to gain by a massive investment in the formalization of mathematical arguments in (say) Lean. (I “say” Lean but I don’t really know what I am talking about or indeed have any idea what “Lean” actually is.) As you know, here at Persiflage we like to put words in people’s mouths which may or may not be a true reflection of their actual beliefs. So let’s say that MH believes that any thing produced by such programs will never produce any insight — or possibly not in anyway that would count as meaningful insights for humans (if a computer could talk, we wouldn’t be able to understand it). KB believes that without the promised salvation of computer verified proofs, modern number theory is in danger of shredding itself before your eyes like that Banksy. What do you think? Since everything comes down to money, the correct way to answer this question is to say what percentage of the NSF budget are you willing to be spent on these projects. Nuanced answers are acceptable (e.g. “as long as some really smart people are committing to work on this the NSF should get ahead of the curve and make it a priority” is OK, “better this than some farcical 10 million pound grant to study applications of IUT” is probably a little cheeky but I would accept it if you put your real name to it).

Let the battle begin!

(Photo credit: I went to Carbondale to see the solar eclipse, but all I saw was this lousy sign. The other is just a random web search for “vintage crazy pants”.)