Sieve Methods

Stream: new members

[Arend Mellendijk]

Have any attempts been made to formalise sieve methods? All I have been able to find is an estimate used in the Unit Fractions project (lemma 2.9) that was made using the sieve of Eratosthenes-Legendre.

I ask because I've been learning lean in my free time and I'm at the point now where I should try to work on a larger project. I think it might be fruitful to formalise a proof of Brun's theorem by way of the Selberg sieve. These can be proved using almost entirely elementary methods, so they seem like a reasonable target for formalisation.

Thanks!

[Yaël Dillies]

There has been interest in formalising Maynard's sieve. I would personally like having it because it is a prerequisite to Infinite partial sumsets in the primes. I am ticking off another prerequisite, Bergelson's intersectivity lemma, in #18732

[Kevin Buzzard]

My impression is that this kind of mathematics is perhaps more talked about in the Xena Discord (a private chat) than here, which is not really a good outcome. Maybe it's time for a dedicated analytic number theory stream here? The Bloom-Mehta formalisation of Bloom's unit fractions result is one of mathlib's greatest successes I think -- contemporary maths being formalised in real time.

[Kevin Buzzard]

Indeed one could argue that the success of the unit fractions project is evidence that this area is ripe for interesting formalisation projects.

[Arend Mellendijk]

An update on this: I went ahead with my plan to formalise the Selberg sieve, and I've just finished proving (the simple version of) the Fundamental Theorem of the Selberg Sieve. You can find the repo here, with the main result here.

My next goal is to prove Brun's theorem, or perhaps just that pi(x) << x/log x to convince myself I've actually proved something useful. There is also another version of the fundamental theorem that's more intuitive to apply, but it relies on Mertens' third theorem both in proof (as far as I know) and application. Since Mertens' theorems aren't in mathlib yet I'm holding off on implementing that for the moment.

I'd like to know what people think about adding a result like this to mathlib. It would take quite a bit of refactoring in its current form, as I haven't put much time into optimisation or using a style consistent with mathlib. I'd also be worried that the result is a little too specific. As it stands it's ~2000 (ungolfed) loc for a single result that doesn't do much to build a larger theory. That said if people are interested I'd definitely be willing to work on getting this code in shape.

[Yaël Dillies]

cc @Bhavik Mehta

[Yaël Dillies]

Maynard sieve next? :smiley:

[Arend Mellendijk]

I won't say I haven't considered it...

[Arend Mellendijk]

But frankly I'd need to read up on the proof of Bombieri-Vinogradov before I commit to anything.

[Arend Mellendijk]

Second update: I've just finished proving

theorem primeCounting_isBigO_atTop : (fun N => (π N:ℝ)) =O[atTop] (fun N => N / Real.log N)

so at least I've convinced myself I've proved something nontrivial. I realise the result itself will probably be overshadowed by the prime number theorem relatively soon, but most of the additional work came from a bound that will be useful for other simple sieve problems (like Brun's theorem). I'll definitely work to clean up the code for that bound and get it merged into mathlib.

[Thomas Bloom]

This is great! (Apologies for the late response, I only just saw this thread.)

As you say, the most that I know of are the sieve-type estimates that Bhavik and I formalised for unit fractions. This is essentially Eratosthenes-Legendre. I'm very glad to hear that the Selberg sieve has been formalised.

For your prime big-O bound, just so you're aware, @Bhavik Mehta proved this via Chebyshev's estimates (also for unit fractions), not sure if this is in mathlib yet?

I'd say that Selberg sieve should definitely be in mathlib, it's used all the time in analytic number theory.

For a next project, how about the combinatorial sieve? e.g. Beta sieve. A little technical to write down the statement, but if anything the proof is actually step-by-step simpler than Selberg's, and is often more powerful.

re: Bombieri-Vinogradov, before that's done, we need to formalise Vaughan's identity (https://en.wikipedia.org/wiki/Vaughan%27s_identity - just the elementary arithmetic function statement, ignore the version involving the zeta function). This is essential to a simple proof of B-V, and indeed is another everyday tool of analytic number theory that belongs in mathlib. (e.g. would be needed to formalise a proof that all sufficiently large odd numbers are the sum of three primes).