Minkowski Lattice Theorem

Stream: Is there code for X?

[Yaël Dillies]

Is anybody already working on Minkowski's theorem? https://en.wikipedia.org/wiki/Minkowski%27s_theorem
I'm thinking of formalising it.

[Johan Commelin]

I think @Alex J. Best has a PR on (parts of?) it

[Johan Commelin]

#2819

[Yaël Dillies]

Oh right, thanks! This seems a bit dead, though :frown:

[Alex J. Best]

@Yaël Dillies yes, it is quite dead! At the time I came to the conclusion that measure theory needed more development to prove some of the key results, https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/random.20PR.3A.20.5BWIP.5D.20feat.28number_theory.2Fgeometry_of_numbers.29.3A.2E.2E.2E/near/215254314 I think a lot of this is now possible thanks to the work of many people (lots of credit to Floris and Yury though!). So I definitely think its high time to revive this PR, or rewrite it completely lol. I think I will have more time for lean in the next few weeks (I just submitted my PhD thesis today!) so I'm happy to collaborate on this :smile:.

[Johan Commelin]

Congrats on submitting your thesis! :tada:

[Yaël Dillies]

I would love to collaborate with you on it! To put in context, I'm looking for a nice result (if possible in combinatorics) to formalize during my summer internship with Bhavik Mehta. How much time do you think still need to be poured in to make the proof work?