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

[Buzzard, Kevin M]

Sorry for flooding -- I meant to also comment on this:

[Friedman]:
ME:

At what stage in the process a-e below would you think a serious
professional mathematician would want to use yours and any other
"proof software" to help when mired in state of the art details they
just barely understand themselves and where until normally final
stages, practically every statement is flawed?

a. Getting a Theorem proved in the sense of before any manuscript,
where the "proof" lies in mental images and scribbles on a piece of
paper or computer screen. Before any serious checking.
b. In the serious checking stage before writeup.
c. In the writeup stage constructing a first manuscript meant to
"verify" that it's all there for me only. Generally no one else would
get much out of it.
d. Perfecting the writeup so that it can be used to give a detailed
seminar presentation somewhat understandable to some experts other
than the author..
e. Perfecting the writeup further turning it into a real preprint
publicly available so advanced students can really get a good sense of
what is going on.

***

This question assumes that mathematics will continue to be done the
way it has been done in the past. What I envisage is that the
experimentation process​ i.e. before even part a, will be done, in some
subject areas (which areas? depends on who we get on board) using
proof assistants. They will be intimately involved in the process from
the beginning and will become part of the human creative process.
I envisage large, computer-searchable, machine-learnable,
databases of mathematical facts being accessible to everyone. The big
debate amongst the CS people is "well, which system? Maybe we should
make a new system which joins up other systems?" etc etc. My answer
to this right now is to see what we can do in Lean and if the CS people
come up with good reasons to use another system then we can worry
about that later. In four years we've made most of an undergraduate
curriculum and now more people are appearing the growth rate is
increasing. Once things like the statements​ of the stacks project
https://stacks.math.columbia.edu/  are formalised it is trivial to make
powerful search. Once things like the proofs​ are formalised (a far
harder project) we can start thinking about computers coming up
with proofs in algebraic geometry for themselves. If logicians want
to start formalising various encyclopedic texts in e.g. set theory then
it is not hard to figure out how to start, e.g. https://leanprover-community.github.io/ .

Kevin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210226/b75ae129/attachment-0001.html>