Zulip Chat Archive

Stream: Is there code for X?

Topic: Minkowski Lattice Theorem


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 16 2021 at 13:01):

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

view this post on Zulip Johan Commelin (Apr 16 2021 at 13:02):

#2819

view this post on Zulip Yaël Dillies (Apr 16 2021 at 13:07):

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

view this post on Zulip 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:.

view this post on Zulip Johan Commelin (Apr 16 2021 at 17:23):

Congrats on submitting your thesis! :tada:

view this post on Zulip 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: May 17 2021 at 15:13 UTC