Advice sought on formalizing Selberg sieve weight properties

Stream: mathlib4

[Bob Jefferson]

Hello everyone,

I’m an independent researcher working on a formalization project in Lean 4 related to sieve methods in analytic number theory. My goal is to rigorously verify properties of Selberg sieve weights used to study prime pairs.

At this stage, I’m focusing on formalizing the Selberg sieve weights themselves — specifically:

• Their definition based on squarefree divisors and Möbius and Euler totient functions

• Basic properties like non-negativity, boundedness, and support only on certain divisor sets

• Handling of sieve level parameters $D = \lfloor N^\theta \rfloor$

Below is a minimal snippet illustrating the current definition and a simple lemma about non-negativity:

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Fintype.Basic

open Finset Nat

def sieveLevel (θ : ℝ) (N : ℕ) : ℕ := Nat.floor (N ^ θ)

def selbergWeight (D : ℕ) (n : ℕ) : ℝ :=
  (∑ d in (range (D + 1)), if Squarefree d ∧ d ∣ n then (μ d : ℝ) / φ d else 0) ^ 2

lemma selbergWeight_nonneg (D n : ℕ) : 0 ≤ selbergWeight D n := by
  apply pow_two_nonneg

I’d appreciate any pointers on:

• Existing Mathlib lemmas or tactics to help with proving support and boundedness

• Best practices for handling dynamic parameters like sieve levels in Lean

• Relevant prior formalizations of sieve methods or analytic weights

Thank you very much for your help!

[Kenny Lau]

Please use 3 #backticks to ensure that your code is properly formatted.

[Ruben Van de Velde]

Are you aware of the work on sieves in https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/ ?

[Bob Jefferson]

Hi, thanks so much for pointing me to Alex Kontorovich’s Prime Number Theorem repository — this looks like a very promising resource!

I plan to review the analytic number theory arguments there, especially around sieve bounds, Mertens-type sums, and error term estimates, as these are exactly the areas where my current formalization needs reinforcement.

If anyone here has experience working with this repo or formalizing similar analytic results in Lean 4, I’d love to hear about your approaches or any tips you might share.

Meanwhile, I will explore how to adapt some of these classical results into constructive, machine-verified lemmas to replace the placeholders in my project.

Thanks again for the pointer — this community is invaluable!

[Michael Rothgang]

@Arend Mellendijk

[Terence Tao]

We have a dedicated channel for the PNT project at #PrimeNumberTheorem+ , which would be a logical place to make more specific inquiries.

We did import some Selberg sieve machinery from https://github.com/FLDutchmann/selberg-sieve4/tree/1f56eaf10bdf7c2e4808e42b40e1a7e947490917 at one point, but currently I believe we do not use that dependency. But the code there may be more directly useful for your own project.

[Bob Jefferson]

Dear Professor Tao,

Thank you very much for your kind response and for pointing me toward the #PrimeNumberTheorem+ channel — I will certainly join there to continue more focused discussions.

I appreciate the reference to the Selberg sieve code by FLDutchmann. I’ll study that repository closely, as it may indeed provide useful components or inspiration for strengthening the analytic and sieve-theoretic aspects of my Lean formalization project.

Your guidance is invaluable, and I look forward to engaging further with the community in the dedicated channel.

Thank you again for your time and support.