Density conjecture on unit fractions

Stream: general

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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]

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]

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]

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]

Amazing!

[Patrick Massot]

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

[Bhavik Mehta]

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]

I'll update it now

[Patrick Massot]

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

[Bhavik Mehta]

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]

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

[Bhavik Mehta]

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]

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]

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]

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

[Ruben Van de Velde]

Is the PRing something you could use help with?

[Thomas Bloom]

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

[Bhavik Mehta]

@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]

Ah right, sorry my mistake.