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

Mario Carneiro di.gama at
Mon Mar 1 02:39:11 EST 2021

On Sun, Feb 28, 2021 at 9:08 PM Paul Blain Levy <p.b.levy at> wrote:

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

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>

More information about the FOM mailing list