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

[Buzzard, Kevin M]

> Just as a thought experiment. Where exactly in this process would
> somebody being the original author proving the Invariance of Domain
> (topology) or the Consistency of the Continuum Hypothesis or the
> Existence of an RE set of Intermediate Degree, use yours or any other
> proof management software?

As a non-thought-experiment, independence of CH is done in Lean
not by some team of computer science professors (like the odd
order theorem) but by a PhD student and a post-doc here:

https://florisvandoorn.com/papers/flypitch-cpp-2020.pdf

Theorem provers are real and they are coming to eat you. Wake up.

> Maybe you should consider focusing on targeting the special situations.

It is very easy to take an arbitrary piece of formalised mathematics and
call it, a posteriori, a "special situation". The fact that you named
consistency of CH explicitly, thus implying it's not a "special situation",
and it turns out to be formalised anyway, weakens your argument.
Someone contacted me offline and said that this theorem of Scholze
is perhaps also a "special situation", but if relevant important mathematics
by a Fields Medal winner is deemed a "special situation" then by this
point I think one does not even care about the notion, whatever it even means.

Kevin

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