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

Paul Blain Levy p.b.levy at
Sun Feb 28 08:18:26 EST 2021

Dear Kevin,

Has anyone proved Borel determinacy in Lean?

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).


> Date: Fri, 26 Feb 2021 10:19:00 +0000
> From: "Buzzard, Kevin M" <k.buzzard at>
> To: Foundations of Mathematics <fom at>
> 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:
> 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

More information about the FOM mailing list