Zulip Chat Archive

I would like to write some number theory and/or additive combinatorics in lean, mostly to acclimate myself with using a theorem prover. Would anyone be interested to join me? I am open specific topics. Ideally, I would like someone who has some experience with theorem provers, as my experience is limited to the natural number game and the 9 exercise sets from the lean tutorials.

Johan Commelin (Mar 07 2022 at 17:54):

Welcome! I don't really know this part of maths. But it seems like Cauchy-Davenport is a fundamental result, and I don't think that has been formalized in Lean. How hard is the proof mathswise?

Johan Commelin (Mar 07 2022 at 17:54):

Probably @Bhavik Mehta and @Yaël Dillies are good people to talk to.

Bhavik Mehta (Mar 07 2022 at 17:57):

Welcome! You might also like to talk to @Thomas Bloom who I think may have a very similar mathematical background to you and a little bit of experience too

Thomas Bloom (Mar 07 2022 at 18:06):

Hi George! Indeed, I was just speaking to Bhavik a few days ago about formalising more additive combinatorics in Lean. (Bhavik has already formalised Solymosi's 5/4 sum-product exponent for sets of reals.)

One quite attainable project is to formalise a proof of a Freiman inverse result for subsets of F_p^n. The main steps here would be:

Ruzsa Triangle Inequality
Petridis' proof of Plunnecke inequality
Ruzsa covering lemma
A couple of elementary facts about vector spaces, that hopefully are already in Lean somewhere anyway.

I think probably formalising a proof of the Ruzsa Triangle inequality would be both very useful, and also a not-too-difficult exercise in learning how to use Lean beyond the tutorials you mentioned.

George Shakan (Mar 07 2022 at 18:08):

Thank you all for the extremely quick and friendly responses!

@Johan Commelin Cauchy Davenport is quite easy to prove, I even covered it in an undergraduate course.

Thomas Bloom (Mar 07 2022 at 18:09):

(And if you want to see an example of analytic number theory being done 'live' in Lean, Bhavik and I are currently working through formalising my recent paper on unit fractions, see https://b-mehta.github.io/unit-fractions/blueprint/index.html. This is an expanded 'blueprint' for reference when writing the Lean proofs, and if you hover over a Theorem's statement you should see a 'LEAN' thing appear for many of them, and clicking that will take you to the relevant piece of Lean code, where it's written.)

Yaël Dillies (Mar 07 2022 at 18:12):

Bahvik and I also formalized Szemerédi's regularity lemma and Roth's summer last summer and are somewhat planning on formalizing Szemerédi's theorem this summer.

Bhavik Mehta (Mar 07 2022 at 18:12):

I also formalised Behrend's lower bound on sets with no 3APs, and Yaël and I proved the little-o version of Roth's theorem using the regularity lemma, so you have some idea of what else is achievable; a couple of years ago the solution to the cap-set problem was also formalised