Zulip Chat Archive

Stream: new members

Topic: Gabin Kolly

Gabin Kolly (Apr 23 2023 at 19:30):

I'm new and currently going through the Mathlib3 tutorial. I'm beginning a Master's thesis on formalizing Model Theory in Lean, with the goal of helping to formalize basic definitions and theorems. It seems that most of what has been done in Model Theory in Lean3 has not been ported to Lean4 for the moment. Since I will work on that project part time for the next 12 months, should I begin right away by doing everything in Lean4? That would probably mean that I should begin by helping to port the rest of Model Theory.

Yaël Dillies (Apr 23 2023 at 19:36):

Do you know about Flypitch? This hasn't been ported.

Adam Topaz (Apr 23 2023 at 20:01):

The main statement of flypitch (independence of CH) hasn’t been moved to Mathlib as far as I know. But a lot of the basic model theory already has. It seems that the mathlib port will be done in a few months. Personally, I think that focusing on lean4 is the right choice, and porting model theory from mathlib3 to mathlib4 would be a great place to start.

Kevin Buzzard (Apr 23 2023 at 21:55):

There's also this project done by an Imperial student: https://github.com/Jlh18/ModelTheoryInLean8/ . It proves Ax-Grothendieck in Lean 3.

Gabin Kolly (Apr 24 2023 at 17:00):

Thank you for the pointers!
Is there a reason why frypitch has not been moved to Mathlib? Is it just because of the work needed to adapt everything to the mathlib style? I haven't found something on what is accepted in Mathlib (would a proof of the independence of CH be accepted, or is it too specific?)

Patrick Massot (Apr 24 2023 at 17:01):

@Floris van Doorn, this is a question for you.

Ruben Van de Velde (Apr 24 2023 at 17:46):

I've seen some mentions of flypitch in mathlib - not sure if they were a sign of the work slowly getting merged or it was new code inspired by it

Yaël Dillies (Apr 24 2023 at 17:46):

Some code has moved to mathlib, yeah, but it's a slow process.

Floris van Doorn (Apr 24 2023 at 17:47):

The code in Flypitch indeed did not follow the mathlib style, and we used various shortcuts and temporary hacks in our proofs.
As Adam said, a lot of the basic model theory was ported to mathlib (and improved!) by @Aaron Anderson.

Floris van Doorn (Apr 24 2023 at 17:48):

The model theory code in mathlib is new code inspired by flypitch, improving some of the pain points, and making some definitions more generally applicable.

Aaron Anderson (Apr 24 2023 at 18:16):

In particular, that code is just my attempt to beat the quickest path (using a ton of flypitch work) towards the kind of model theory I do research on.

Aaron Anderson (Apr 24 2023 at 18:27):

I haven't added much in a while, but I have a lot of thoughts for how to move forward, which I'd be happy to discuss!

Last updated: Dec 20 2023 at 11:08 UTC