Proof Assistants being seriously useful for everyday garden variety serious mathematical developments
Buzzard, Kevin M
k.buzzard at imperial.ac.uk
Fri Feb 26 05:19:00 EST 2021
> 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:
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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM