Zulip Chat Archive

Stream: general

Topic: Density conjecture on unit fractions

Bhavik Mehta (Feb 04 2022 at 21:59):

Together with @Thomas Bloom I've been working on a formalisation of his December 2021 preprint https://arxiv.org/pdf/2112.03726.pdf, which solves a 1980 conjecture of Erdős and Graham. The project can be found here: https://b-mehta.github.io/unit-fractions/. Here are some of the reasons I'm really excited about this:

  • Some of the prerequisites for the paper are things that I first learnt from Thomas' Part III course at Cambridge!
  • The result is pretty understandable: any dense set of integers contains distinct integers whose reciprocals sum to 1, but also a very recent piece of mathematics, and involves stuff from number theory, combinatorics and analysis
  • This is the first formalisation project I'm aware of where the author of the paper is actively involved in writing the formalisation: the majority of the theorem statements which are <= 3 away from the main results on the blueprint (log_density_theorem and density_theorem) were written by Thomas!

Please let one of us know if you'd like to help out! For the moment, I think it should be a small enough project not to warrant a separate stream, but perhaps that will change.

Floris van Doorn (Feb 05 2022 at 00:02):

Cool! Btw, you want to remove the square brackets around your first link.

Bhavik Mehta (Feb 05 2022 at 00:16):

Oops, I messed up the URL notation, thanks for that!

Kevin Buzzard (Feb 05 2022 at 07:13):

I think Neil Strickland has formalised part of one of his own papers, as has Bjorn Kjos-Hanssen. However neither of them were proving a conjecture of Erdos. I agree with Bhavik, I think this would be an important milestone. "The author proved a conjecture of Erdos, learnt lean and then verified their proof in lean with the help of a member of the community". That's really a unique story and shows what can be done right now. I really hope you guys can get the proof formalised!

Alex J. Best (Mar 09 2022 at 20:19):

A nice quanta article just came out on @Thomas Blooms work https://www.quantamagazine.org/maths-oldest-problem-ever-gets-a-new-answer-20220309/, worth checking out if you want some more background for the ideas behind this project!

Johan Commelin (Mar 09 2022 at 21:06):

I also notice that https://b-mehta.github.io/unit-fractions/blueprint/dep_graph.html seems to have quite a lot of green already.
(Btw, if you want a more detailed legend for the graph, you can update to the latest version of the lean-blueprint package.)

Bhavik Mehta (Jun 12 2022 at 20:27):

Thomas and I are very happy to announce that the main theorem has been completely proved! The original conjecture, as mentioned in the Quanta article,

theorem unit_fractions_upper_density (A : set ) (hA : upper_density A > 0):
    (S : finset ), (S : set )  A   n in S, (1 / n : ) = 1 :=

is now totally sorry free. And this was finished before the referee report on the paper proving it has been returned!
Along the way, we used the Hardy-Littlewood circle method, which hasn't been verified in any formal proof before (to the best of my knowledge), and formalised a ton of analytic number theory (most of the first section of the Part III analytic number theory course), plus some tighter estimates such as Wigert's theorem here: https://en.wikipedia.org/wiki/Divisor_function#Growth_rate. Plus, we think this is the first one of Erdős' prize conjectures to have a formalised solution!
The process made me learn a lot more about how filters and integration work in Lean, but I think what's really exciting about this is that a huge portion of the formalisation was done by Thomas himself, who knew absolutely no Lean 6 months ago.

Patrick Massot (Jun 12 2022 at 20:30):


Patrick Massot (Jun 12 2022 at 20:31):

Why is https://b-mehta.github.io/unit-fractions/blueprint/dep_graph.html still full of blue?

Bhavik Mehta (Jun 12 2022 at 20:32):

Patrick Massot said:

Why is https://b-mehta.github.io/unit-fractions/blueprint/dep_graph.html still full of blue?

Because near the end we stopped updating it!

Bhavik Mehta (Jun 12 2022 at 20:33):

I'll update it now

Patrick Massot (Jun 12 2022 at 20:36):

And now the standard question: how far are you from PRing all the general purpose stuff to mathlib?

Bhavik Mehta (Jun 12 2022 at 20:38):

It may be slow, but in theory all manageable. Certainly all the analytic number theory would be valuable to mathlib, indeed I've already PR'd some of the important parts.

Michael Stoll (Jun 12 2022 at 20:44):

Could this be used to get the prime number theorem and Dirichlet's theorem on primes in AP?

Bhavik Mehta (Jun 12 2022 at 20:46):

The blueprint is now updated, and it also now compiles on current mathlib HEAD (as of writing)! Once the website updates, every item should be green, save for log_density_theorem: this corresponds to Theorem 3 from the paper, which is a consequence of the methods used to prove Theorem 2 density_theorem, which is the main result. We're hoping to prove Theorem 3 next, but the key conjecture was Theorem 2

Bhavik Mehta (Jun 12 2022 at 20:47):

Michael Stoll said:

Could this be used to get the prime number theorem and Dirichlet's theorem on primes in AP?

Not directly, though hopefully the analytic number theory techniques (such as partial summation) should be helpful to formalise an elementary proof of the prime number theorem. The proof I know of for Dirichlet uses some complex analysis, which didn't show up at all here so I don't expect it to be useful.

Patrick Massot (Jun 12 2022 at 20:53):

It would be awesome to have a blog post about this adventure on the community website (before having a real publication). And I'm sure Quanta will love this story, you should definitely tell them.

Yaël Dillies (Jun 12 2022 at 21:01):

@David Loeffler, your work will have direct applications here! The unit fractions project needs the Basel problem.

Ruben Van de Velde (Jun 12 2022 at 21:13):

Is the PRing something you could use help with?

Thomas Bloom (Jun 12 2022 at 21:48):

@Yaël Dillies I don't think the Basel problem is used anywhere in unit fractions?

Bhavik Mehta (Jun 12 2022 at 22:22):

@Yaël Dillies The Basel problem isn't needed anywhere, I just did that one day to test that I did actually understand specific analysis in Lean!

Yaël Dillies (Jun 13 2022 at 00:10):

Ah right, sorry my mistake.

Last updated: Aug 03 2023 at 10:10 UTC