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

[Paul Blain Levy]

In that case I take back my comment.    I was thinking of Martin-Loef 
style systems such as Agda, and didn't realize that Lean is 
significantly different.  Thanks for your explanation, Mario.

Paul

> Date: Mon, 1 Mar 2021 02:39:11 -0500
> From: Mario Carneiro <di.gama at gmail.com>
> To: Paul Blain Levy <p.b.levy at bham.ac.uk>
> Cc: Foundations of Mathematics <fom at cs.nyu.edu>
> Subject: Re: Proof Assistants being seriously useful for everyday
> 	garden variety serious mathematical development
> Message-ID:
> 	<CAFXXJSuZhYP4M+B9xseembprTHvyCXQnJF2=55AHQmfYq4J4kg at mail.gmail.com>
> Content-Type: text/plain; charset="utf-8"
>
> On Sun, Feb 28, 2021 at 9:08 PM Paul Blain Levy <p.b.levy at bham.ac.uk> wrote:
>
>> 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).
>>
> I encourage you to bring this up on the Lean Zulip if you care to see it
> happen. As far as type theory vs set theory is concerned, I don't think
> lean will have any technical troubles proving this, since lean without
> universes is roughly equivalent to ZFC. Inductive types make up the
> difference as regards lack of a replacement axiom, although the techniques
> are different enough that I'm not sure a straight comparison is possible.
>
> Mario Carneiro