Proof Assistants being seriously useful for everyday garden variety serious mathematical developments

[Timothy Y. Chow]

Sam Sanders wrote:

> I recall a 2013 talk by Georges Gonthier about his formalisation of the 
> odd-order theorem. While this was a celebrated milestone, Gonthier also 
> displayed a picture of the Alps, with the lowest peak marked.  His 
> message was essentially that the odd-order theorem was just the first 
> step as part of much larger project, but that the latter was infeasible 
> at the moment.

I'd be interested in learning more about what Gonthier said.  It makes a 
big difference whether the infeasible "larger project" was the CFSG 
(classification of finite simple groups) or merely the project of 
formalizing more "serious but garden variety" group theory.  The CFSG is 
by no stretch of the imagination "garden variety."  Writing down a 
satisfactory proof of the CFSG *by any means* is bordering on an 
infeasible project.  Back in 1995, Barry Cipra wrote an article in 
"Science" in which he said that experts were predicting that a 
second-generation proof (the GLS project) would span 3000 to 5000 pages. 
The AMS has just published Volume 9 of GLS, and if you count the 
Aschbacher-Smith quasithin work, the 5000-page threshold has already been 
broken.  At least 3 more volumes are needed, and I think the smart money 
is betting that it will be more than 3 (perhaps in the region of 2000 more 
pages).  The last piece of the puzzle as currently conceived, the case 
"e(G)=3" as it's called, is apparently still in flux.  On top of that, the 
major players in the subject are getting on in years and if they are 
unable to complete everything themselves, there is a shortage of younger 
group theorists to pick up the baton.

I am glad to see Kevin Buzzard chiming in.  I think he has put his finger 
on one part of the problem.  Namely, there hasn't been an effort to 
systematically formalize the entire undergraduate curriculum.  If one does 
not have that infrastructure then that is always going to be an annoying 
obstacle.  But Buzzard, to his credit, is focusing on what I think are 
many of the right things---not just formalizing all basic math, but 
training undergraduates and working to make proof assistants more amenable 
to mathematicians and not just computer scientists.

The other elephant in the room is funding.  We can argue all day about the 
merits of this approach or that approach, but at some point, for a 
large-scale engineering project to succeed, money is needed.  Formalizing 
mathematics is unlikely to attract sufficient support unless there is some 
kind of "payoff" (the payoff need not be nakedly financial but it has to 
be something that significant numbers of people care about).  This is a 
topic that we should all probably think harder about.  My opinion is that 
one of the most promising ideas is to use formalized mathematics as a 
database to train machine learning software on.  Josef Urban and others 
have written about this on FOM, and the Formal Abstracts project that I 
mentioned recently also states this goal explicitly.  Formalizing math 
isn't just about checking correctness.  It's about transforming the way 
mathematics is done, and accomplishing things that could not be done 
otherwise.  Now, this may not be the only motivation for proof assistants, 
but until we develop a better vision for what the "payoff" could be, we 
are likely doomed to remain a backwater.

Tim