Gabin Kolly

Stream: new members

[Gabin Kolly]

Hi!
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]

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

[Adam Topaz]

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]

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

[Gabin Kolly]

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]

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

[Ruben Van de Velde]

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]

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

[Floris van Doorn]

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]

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]

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]

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!