Proof Assistants being seriously useful for everyday garden variety serious mathematical developments
Timothy Y. Chow
tchow at math.princeton.edu
Fri Feb 26 09:49:23 EST 2021
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
More information about the FOM
mailing list