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

[Paul Blain Levy]

Dear Kevin,

Has anyone proved Borel determinacy in Lean?

https://en.wikipedia.org/wiki/Borel_determinacy_theorem

If not, I suggest this to the Lean community for two reasons. Firstly, 
the theorem is interesting in its own right.  Secondly, I think that 
formalizing it would help to clarify the difference between a type 
theoretic framework (where one has to use a universe in order to 
compensate for the absence of Replacement) and a set theoretic framework 
(where no universe is required).

Paul

> Date: Fri, 26 Feb 2021 10:19:00 +0000
> From: "Buzzard, Kevin M" <k.buzzard at imperial.ac.uk>
> To: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: Proof Assistants being seriously useful for everyday
> garden variety serious mathematical developments
>> 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
>