Lovasz Local Lemma - mathlib4 Contribution

Stream: general

[Nathan Glover]

Hello, it's been a while, but a year ago I formalized the Lovász Local Lemma in Lean 3.0. I finally translated it to Lean 4.0 (see here), and, if folks think it would be useful, I'd love to add it to mathlib4. I've seen this page and plan on following it closely, but is there anything else I should do or be aware of that isn't mentioned there?

[Nathan Glover]

I might also redo the symmetric corollary to match Lemma III from here; my current symmetric version is sort of a mangled version of Lemmas II and III.

[Nathan Glover]

Also, I have yet to really read through the style guideline pages (I will before continuing with the PR process, don't worry) but is there any chance somebody would be willing to take a quick glance at my code? This is my first time really working with Lean and I'm curious where it lands on the "utterly horrific" to "beautifully perfect" spectrum

[Newell Jensen]

You might as well create a PR. In the review process you will get good feedback. That is my advice at least.

[Nathan Glover]

Okay that sounds good, many thanks!

[Yaël Dillies]

Just going off memory, but I remember @Yves Jäckle's formalisation was more general than yours.

[Kevin Buzzard]

I don't know anything about the mathematics here but a style observation is that it's much more idiomatic in mathlib to have many small proofs rather than one big proof with many haves in. The "one big proof" style is also much harder to work with because every time you add a line lean has to recompile every proof rather than just the one you're working on. Was it hell to write in this style?

On the other hand, lots and lots of comments is a great style :-)

[Nathan Glover]

Yaël Dillies said:

Just going off memory, but I remember Yves Jäckle's formalisation was more general than yours.

Oh I have not seen this; where might I find it? I looked pretty hard to see if anyone else had formalized this result but I guess I didn't look in the right places.

[Nathan Glover]

Kevin Buzzard said:

Was it hell to write in this style?

It wasn't too bad; Lean was smart enough to not recompile the whole thing every time. I rarely had to recompile the entire proof during the process. Regardless, I can agree that that style is better. It's been a while, but I believe the main reason I didn't split it up much is because of the monstrous amount of hypotheses every small lemma would need (and I was never able to get the "variable" thing to work properly for me; perhaps I should've tried harder).

[Newell Jensen]

Usually the proof is the hardest part so if you got that golfing and refactoring shouldn't be too much of an issue for you.

[Yury G. Kudryashov]

A common trick for the case if you have lots of auxiliary lemmas with common assumptions is to put all these assumptions into a structure.

[Yaël Dillies]

Newell Jensen said:

Usually the proof is the hardest part so if you got that golfing and refactoring shouldn't be too much of an issue for you.

I disagree! I spend most of my time making things mathlib-ready and refactoring so that the proof becomes nice and simple.

[Yaël Dillies]

Nathan Glover said:

where might I find it?

It is in https://github.com/Happyves/Master_Thesis and I've just managed to port it to Lean 4 after many failed mathport attempts over the past two months. I'll publish the port soon.

[Newell Jensen]

Yaël Dillies said:

Newell Jensen said:

Usually the proof is the hardest part so if you got that golfing and refactoring shouldn't be too much of an issue for you.

I disagree! I spend most of my time making things mathlib-ready and refactoring so that the proof becomes nice and simple.

I have struggled with trying to prove some things in mathlib that I thought would have been straightforward but then again, that is down to my own ignorance! I suppose if this was quicker for me than yes, I see your point.

[Nathan Glover]

Yaël Dillies said:

Nathan Glover said:

where might I find it?

https://github.com/Happyves/Master_Thesis

This is a really cool thesis Yves Jäckle, and thanks Yaël Dillies for sharing!

On the matter of the LLL, I'm having trouble finding a more general formalization of the result in this repo; the only mention of the LLL I can find is in section 4 of the thesis (reference [7] on page 30), which is my outdated Lean 3 formalization of the LLL. Funny thing, I ran into the ennreal.mul_le_mul issue discussed on page 27 when translating to Lean 4; it was one of the main slowdowns.

[Yves Jäckle]

@Zhu tagging here for the original discussion about LLL.
If you want to do the community a great service, you can try to get LLL into mathib for good !

[Yves Jäckle]

Link to the message with my code and to the original LLL paper, which has the correct version of the standard proof.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/github.20permission/near/476505716