Zulip Chat Archive

Stream: Is there code for X?

Topic: Minkowski Lattice Theorem


Yaël Dillies (Apr 16 2021 at 13:01):

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

Johan Commelin (Apr 16 2021 at 13:01):

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

Johan Commelin (Apr 16 2021 at 13:02):

#2819

Yaël Dillies (Apr 16 2021 at 13:07):

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

Alex J. Best (Apr 16 2021 at 17:22):

@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 (Apr 16 2021 at 17:23):

Congrats on submitting your thesis! :tada:

Yaël Dillies (Apr 17 2021 at 06:35):

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?


Last updated: Dec 20 2023 at 11:08 UTC