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

[Mario Carneiro]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210301/5fc11c21/attachment-0001.html>