Clarification of Skepticism

[Freek Wiedijk]

Dear all,

I have been following this discussion with great interest,
and would like to put in my two cents:

I think that we should distinguish with the mundane
technology of proof assistants like Coq, Isabelle and Lean
on the one hand, and the possibility of a math equivalent
of AlphaZero discovering and proving FLT all on its own
(and maybe discovering undreamt of mathematics) on the
other hand.  Talking about the latter will be clouding a
rational discussion of the former.

Of course there is a spectrum here, people like Josef
Urban are using machine learning to make proof assistants
more powerful (the "hammers"), but still to me these are
different things, and I would like to focus on the former.

As an analogy I would like to propose the following: a
genius concert pianist and hifi music equipment.  So the
concert pianist is the mathematician, and the hifi equipment
is the proof technology.

Now, Harvey seems to be saying things like: "hifi equipment
is only needed for only a few special types of music" and
"hifi equipment will never make great music by itself".
To me that seems to miss the point.  Why does not all music
deserve hifi equipment?  And _of course_ your stereo is not
going to make the music by itself.  That's not what it's for.

To extend the analogy a bit: most people don't feel the need
for hifi equipment that will cost them thousands of dollars,
and are perfectly happy with more mundane music players.
Similarly, for many people going to the trouble to formalize
their proofs (given the current state of the art) probably
will not be worth it.

Another point, of which I don't know whether it has been made
already: in programming language research, formalizing all
proofs in Coq is not very special anymore.  This seems to
happen already in a significant number of papers (and then
those papers are _not_ about the Coq code, the existence
of the Coq formalisation is just mentioned in passing at
the end).  In this community I see a trend that "if you
did not formalize it, you didn't really do the work yet".
So in that field that kind of change seems to be happening.
Now this is about a very different kind of proof from the
kind in pure mathematics, but still it demonstrates that
things _can_ change in some communities.  And once the
"gold standard" for when something has been properly proved
has changed, it is hard to remember how it was before.

Another point, which Jeremy Avigad once made to me: once
formalizing a paper becomes less work than having a referee
check it manually, people will start pushing that work to
the author.  That seems to make sense to me.

I agree with Harvey that you really would like a system
in which experimenting with data, graphing and making
diagrams, _and_ representing the definitions, statements
and proofs is all together.  Currently we have systems
like Mathematica on the one hand, and the proof assistants
on the other hand, and they are not close to merging yet.
(I once had a project to work towards this goal -- it was
called FEAR, formalising elementary analysis rigorously --
but that unfortunately never went beyond a prototype stage.)

Finally, N.G. de Bruijn, who invented the field of proof
assistants in the late sixties, imagined a pyramid with
creative mathematicians like Harvey at the top, a layer
of people who would clarify and work out the ideas below
that, and so on, until there were "formalisers" formalizing
everything at the bottom.  Now of course, at that time papers
were being typed by secretaries, while now most people use
latex themselves.  So that imagine probably does not apply.
But it does seem relevant to what Harvey has been writing.

My opinion is: let everyone do what he/she likes.  If you're
happy without pushing your mathematics to flawlessness by
taking the trouble to code it in a computer that's fine.
If you like to do that, that's fine as well.  It actually
is quite fun, in a computer game like way, but you won't
know until you learn how to do that yourself.

And I agree with Kevin Buzzard that _if_ we keep doing
proofs in mathematics (maybe proving theorems will be a
dying art?), that eventually the proof assistant technology
will become a standard part of this.  And as AlphaZero has
shown, changes in what is possible in computer technology
sometimes are rapid, so who knows how fast this will go?

Freek