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

[Buzzard, Kevin M]

Nobody has proved Borel determinacy in Lean or indeed the much easier open determinacy. These results might be proved in other theorem provers (some of which have been around for longer) but most of the mathematical projects happening right now in lean are not in logic or set theory. I was taught about Borel determinacy by Mathias in a graduate course in Cambridge in the 90s and I am certain that it would be possible to do in Lean. The hard part is finding someone to do it. Open determinacy is something one should do first in order to check that one has the definitions in a usable form. For example it took some thought to get Conway's general notion of a game (in the sense of ONAG) formalised in Lean.

Get Outlook for Android<https://aka.ms/ghei36>
________________________________
From: Mario Carneiro <di.gama at gmail.com>
Sent: Monday, March 1, 2021 7:39:11 AM
To: Paul Blain Levy <p.b.levy at bham.ac.uk>
Cc: Foundations of Mathematics <fom at cs.nyu.edu>; Buzzard, Kevin M <k.buzzard at imperial.ac.uk>
Subject: Re: Proof Assistants being seriously useful for everyday garden variety serious mathematical development


This email from di.gama at gmail.com originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. If you trust the sender, add them to your safe senders list<https://spam.ic.ac.uk/SpamConsole/Senders.aspx> to disable email stamping for this address.




On Sun, Feb 28, 2021 at 9:08 PM Paul Blain Levy <p.b.levy at bham.ac.uk<mailto: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/20210303/ce83b0eb/attachment-0001.html>