Clarification of Skepticism

[Buzzard, Kevin M]

Tim Chow said:

> Even today, I would submit that it may be misleading to ask whether
> programs can perform solo JUMPS a la Evel Knievel.  The more relevant
> question is whether JUMPS are being made that would not be made without
> the program.

What we are discovering when formalising known mathematics are things like
new abstractions. As an example one could look at the description of how to
think about completion in sections 4 and 5 of https://arxiv.org/abs/1910.12320 .
By having a concrete goal (a complex definition of Scholze) we were forced
to formalise a lot of stuff in Bourbaki, and in some places we realised that what
they were doing was suboptimal. This is perhaps an example of some kind of JUMP
which was made not by, but because of, proof assistants.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210321/4ee75014/attachment.html>