Zulip Chat Archive
Stream: general
Topic: Flypitch
Jesse Michael Han (Apr 05 2019 at 02:50):
Hi everyone! I'm pleased to announce that @Floris van Doorn and I have completed a formalization of forcing and the unprovability of the continuum hypothesis.
Our source code is located here. There is some cleaning up to do, but there is a file summary.lean with all the main results and definitions.
We also submitted a paper describing this result to ITP 2019, and welcome your comments!
(We also now have a website which looks suspiciously similar to leanprover.github.io)
Scott Morrison (Apr 05 2019 at 03:21):
on https://flypitch.github.io/about/, "As of April 2018," should be 2019.
Jesse Michael Han (Apr 05 2019 at 03:22):
good catch, thanks!
Jesse Michael Han (Sep 20 2019 at 03:50):
@Floris van Doorn and I have completed a formal proof of the independence of the continuum hypothesis!
David Michael Roberts (Sep 20 2019 at 05:13):
In just over a year! Not bad, starting from having to define first-order logic and work up from there.
David Michael Roberts (Sep 20 2019 at 05:14):
I note that now number 24 here http://www.cs.ru.nl/~freek/100/index.html can be ticked off the list. Nice to see Lean has two proofs no other system has.
Johan Commelin (Sep 20 2019 at 06:16):
@Freek Wiedijk :up:
Kevin Buzzard (Sep 20 2019 at 07:19):
Best get cracking on Fermat, Jesse ;-)
Patrick Massot (Sep 26 2019 at 15:29):
Those days in every French train station newspaper and magazine kiosks, you can see this. The headline translates to "Towards a new theory of infinity. The continuum hypothesis soon proved?".
Patrick Massot (Sep 26 2019 at 15:30):
You can get a preview at https://www.pourlascience.fr/sd/mathematiques/en-finir-avec-lhypothese-du-continu-17963.php.
Patrick Massot (Sep 26 2019 at 15:31):
It does mention Gödel and Cohen's proofs, but reports on people trying to find nice axioms to add to ZF in order to prove CH.
Patrick Massot (Sep 26 2019 at 15:32):
Too bad Flypitch doesn't seem to be mentioned.
Johan Commelin (Sep 27 2019 at 04:46):
I know of a really nice axiom that one can add to ZF in order to prove CH :rolling_on_the_floor_laughing:
Patrick Massot (Sep 27 2019 at 08:06):
They do discuss that possibility, but they don't like it. They want only axioms that look true, especially axioms asserting existence of large cardinals, and axioms saying that every set can be constructed by some process. If I understand correctly, non-CH is unfortunately compatible with all large cardinal axioms. And restricting too much the allowed constructions rules out some large cardinals, so they are looking for some magic restrictions.
Mario Carneiro (Sep 27 2019 at 08:17):
what is V = L ultime?
Mario Carneiro (Sep 27 2019 at 08:18):
most large cardinal axioms have nothing to say about CH or GCH one way or another
Patrick Massot (Sep 27 2019 at 08:35):
Yes, that's the unfortunate part. At this stage, it's probably more efficient to read some serious source, maybe https://link.springer.com/article/10.1007/s00407-014-0142-8?
François G. Dorais (Sep 27 2019 at 11:21):
See this write up by Woodin for a brief outline: http://logic.harvard.edu/EFI_Woodin_StrongAxiomsOfInfinity.pdf
Ultimate L is Woodin's latest attempt at resolving CH (in the positive direction). An earlier attempt of his would have resolved CH negatively, but Woodin determined that this approach wasn't right since it made the universe too "boring" in a sense.
This has little to nothing to do with flypitch yet. We would need a lot more about forcing, relative constructibility, mice and extenders, universally Baire sets, and more to get started with Ultimate L.
Jesse Michael Han (Nov 27 2019 at 17:54):
Floris van Doorn and I have completed a formal proof of the independence of the continuum hypothesis!
Our paper describing this result was accepted to CPP 2020!
The mathlib and lean-perfectoid-spaces papers were also accepted.
Yaël Dillies (Sep 27 2022 at 12:44):
Why is Flypitch not on the list of projects using Lean? That looks like an obvious omission.
Kevin Buzzard (Sep 27 2022 at 16:46):
It's on the front page of the community website so I'm very surprised it's not on the list
Floris van Doorn (Oct 03 2022 at 13:31):
It should be on the list. Can someone with merge power look at leanprover-contrib/leanprover-contrib#20?
Patrick Massot (Oct 03 2022 at 13:38):
I just wrote a comment.
Patrick Massot (Oct 03 2022 at 13:39):
And I don't know who has merge power there. Probably @Rob Lewis?
Ruben Van de Velde (Oct 03 2022 at 13:43):
Maybe @Eric Wieser too?
Last updated: Dec 20 2023 at 11:08 UTC