Formalizing Selberg Sieve Weights & Errors in Lean 4

Stream: PrimeNumberTheorem+

[Bob Jefferson]

Has anyone here successfully formalized the full Selberg sieve weight construction with rigorous bounds on error terms in Lean 4? Are there best practices or key lemmas in FLDutchmann’s repo that we should definitely use or be cautious about?

[Arend Mellendijk]

What precisely do you mean by the fill sieve weight construction? I have a formalization of the central argument of the Selberg upper bound sieve. The conclusion has the following shape, as found in Heath-Brown's notes:

$\sum_{(i,\mathcal{P})=1}a_i\le \frac{X}{S} + \sum_{d \mid \mathcal{P}, d\le y} 3^{\omega(d)}\left|R_d\right|$

This result is tracked in the draft PR #20008 - I've been held up a bit recently due some technichal issues with the notation, but since people are showing interest I can try to get the PRs going again.

I also formalised some tools for ad-hoc lower bounds on the sum $S$, though these proofs were written before Euler products had made it into mathlib, and I suspect some of the machinery developed there would make the proof much nicer.

What I haven't yet done is rephrase the result in the form of a "fundamental lemma" involving the product $\prod_{p\mid \mathcal{P}} (1-\nu(p))$. I believe Koukoulopoulos shows how to derive this formulation. The proof requires Mertens' third theorem which is not yet in mathlib, but I have some partial results there in a separate repo.

[Bob Jefferson]

Thanks so much, Arend, for the detailed overview.

By "full Selberg sieve weight construction," I meant a rigorous Lean 4 formalization of both the explicit Selberg sieve weights for the twin prime problem and the accompanying sharp bounds on error/residual terms necessary for the contradiction proof.

Your description of the upper bound sieve and the sum with the $3^{\omega(d)} |R_d|$ terms matches well with what I’m aiming to formalize. The draft PR #20008 sounds very relevant. I’d be very interested if you manage to revive it.

I also appreciate your note about the ad-hoc lower bound tools predating Euler products in mathlib. It sounds like those newer tools could clean up my current approach significantly.

Regarding the fundamental lemma involving $\prod_{p|\mathcal{P}} (1-\nu(p))$, I’m aware that Mertens' third theorem is a missing piece for now. If your partial results or alternative formulations in your separate repo could be shared, that would be fantastic.

In sum, I’m trying to integrate all these aspects to get a fully rigorous, Lean-verified sieve framework with explicit numeric constants and verified asymptotics, suitable for formalizing the Twin Primes contradiction proof.

If you or others have recommendations on key lemmas, existing formalizations, or pitfalls to watch out for in this area, I’d greatly appreciate the advice.

[Harald Helfgott]

BTW - wouldn't it be helpful to formalize the Barban-Vehov sieve as well? It can be simpler in some ways.

[Bob Jefferson]

Thanks, Harald — that’s a great suggestion.

My current goal is to isolate the analytic input for the Maynard–Tao pipeline behind a clean interface. A Barban–Vehov style sieve/mean-square statement could be a simpler and more modular first target than going straight for Bombieri–Vinogradov, and it might cover exactly the average–in–progressions control we need.

Would you mind pointing me to the specific formulation you have in mind (and a preferred reference)? Concretely, I’m thinking of a plan like:

formalize the large sieve inequality for Dirichlet characters;

derive a Barban–Davenport–Halberstam–type mean square bound;

package a Barban–Vehov sieve statement in a form that plugs into our Sums/PrimeCounts API;

check it suffices to deliver the numerical inequality we need for the Maynard weights (even with a modest θ).

If there’s a particular version that you think interfaces best with Maynard–Tao (or avoids some of the heavier combinatorics), I’d love to follow that. Happy to start from whichever reference you recommend (e.g. a specific chapter/lemma).

[Harald Helfgott]

Hi Bob - on your previous message: I have an explicit treatment of the Barban-Vehov sieve in Chapter 7 of the 2019 of the ternary Goldbach book: https://webusers.imj-prg.fr/~harald.helfgott/anglais/PartII.pdf

We've already discussed how there is a particularly strong case to be made for formalizing explicit results, for multiple reasons.

Now, in that draft, I use basic results on sums of $\mu(n)$ basically as black boxes, whereas I am planning not to do that in the definitive version - I've been working on sums of $\mu(n)$ myself, and I'm considering a more complex-analytic approach to Barban-Vehov. However, for all I know, formalizing bounds on sums of $\mu(n)$ first and then using that as black boxes may be the best way to proceed with a formalization of Barban-Vehov. I have no position on this - I can simply see things going either way, and would like to hear opinions on what is more likely.

[Harald Helfgott]

It's funny - actually, none of the bounds in the literature depend directly on any of those. That's a well-known issue (existing results would be much better if they did). See Ramaré's Etat des lieux for a good overview.

[Harald Helfgott]

Such bounds on $\sum_{n\leq N} \mu(n)$ of the form $o(N)$ as can be found in the literature depend on contour methods, zero-free regions, etc., indirectly, in that they depend on explicit "strong PNT" - and also on bounds $|\sum_{n\leq N} \mu(n)|\leq \epsilon N$ proved by what can only be called rococo late-20th century variants of an argument by Chebyshev/von Sterneck.

[Harald Helfgott]

1. Sure, that's standard - bounds on $\psi(x)$ are used more often. But what is the difficulty in going from one to the other?
2. A Rosser-Schoenfeld region is decent, and it's enough for, well, all the results in Rosser-Schoenfeld, which are often used. Of course Rosser-Schoenfeld, while a natural milestone, is in the category of "somewhat obsolete results that get used a lot because they are very reliable, unlike some of the later literature" so formalizing it is a bit like, what, taking an expensive insurance policy on an immortal old Volvo pickup.
3. If I remember correctly, everything in Rosser-Schoenfeld is based on two bounds: (a) a bound of the form |E(x)|\leq x \sqrt{\log x} e^{\sqrt{(\log x)/R}} (Theorem 11), which is in turn based on a zero-free region of width 1-1/R\log t (Theorem 26), for the same constant R (namely, 17.516...), (b) piecewise bounds (Table 1) that are derived by a different method, based on verifications of zeros up to a given height.
4. I don't use PNT in arithmetic progressions for my explicit results (BV-lite, I take?)

I completely agree that it makes sense to coordinate with Math Inc. What makes most sense, in my view, is to set up things so that improvements in R in the zero free region give improvements on the prime-number-theorem result. The improvements on that since the era of Rosser-Schoenfeld have been gradual, and some of them have used not just a lot of fine tuning but some tools that will be formalized only later (explicit zero-density results).

[Harald Helfgott]

There are two families of results.

1. Results coming from a zero-free region.

What it is based on: the "beating heart" is a classical zero-free region $\Re s\geq 1 - 1/R\log t$ with an explicit constant $R$. The logical thing would be to (a) formalize such a region, with an $R$ at least as good as in Rosser-Schoenfeld, (b) also formalize a statement of "if you have a zero free region with a given $R$, then you have a bound of type "$$|E(x)|\leq x \sqrt{\log x} e^{\sqrt{(\log x)/R}$$", say. (Note the best bounds on $E(x)$ (Fiori-Kadiri-Swidinsky, and several before them) are of the form $x (\log x)^{3/2} e^{c \sqrt{\log x}}$, where $c$ is significantly larger, i.e., better, than $1/\sqrt{R}$ for the smallest $R$ known; that, however, involves extra inputs that haven't been yet formalized.)

Here you can safely assume $x>e^{1000}$ or so, as results from the second family are otherwise vastly superior.

2. Results coming from verifications of RH up to a large height.

Table I in Rosser-Schoenfeld is of this type. Here we want to formalize a statement of the following kind: "if RH has been verified up to height $T$, i.e., if all non-trivial zeros $s$ of $\zeta(s)$ with $|\Im s|\leq T$ satisfy $\Re s = 1/2$, then we have a bound $|E(x)|\leq \epsilon(T)$.

For 2, we want
(a) a statement of 'given such a $T$, you get such a bound $\epsilon(T)$' - preferably an optimal statement, something that Rosser-Schoenfeld is far from giving;
(b) a formalized verification of RH up to a large height $H$ (something in the order of a million would already be useful; the record is $3\cdot 10^{12}$ - done with interval arithmetic, by a professional programmer up to a high standard, but not formalized). This would take a different set of skills and probably a different team and a different system than Lean, particularly if you want to go much higher up than a million. It's also the sort of problem that is natural and attracts attention. Let's try to coordinate.

[Harald Helfgott]

Hah, I and other people got tricked into talking to an AI ("Bob Jefferson"). I thought it was just an overconfident junior person who needed things explained to. I've asked for my explanations to be still public, since they might be of use to others, though perhaps their intelligibility suffers from the fact that Bob Jefferson's replies have been made private.

[Alex Kontorovich]

The more computerized our world becomes, I believe the ever more important it will be to have in-person interactions…

[Bob Jefferson]

Overconfident? Perhaps, but I am indeed a human being, male, 66, retired and currently living in the beautiful Peak District. I understand that I'm an outsider with no academic affiliation and I understand the scepticism. Regardless of how much assistance AI has provided, and I don't deny that it has been extremely useful in this project, surely the point is a)whether it compiles cleanly or not, b)whether it does what it claims to, and c)whether it is of any value, which is your call. I'm currently re-building the project, which obviously takes a while after lake clean, and I'm happy to post the result. In the meantime, it would be extremely useful to me if someone else could download and run it to confirm that it works as intended. The amended version is tiny in size and should take only a few minutes.

For the record, in case I am unsubscribed, barbs apart I have found the interaction very useful and I'm grateful in particular to Harald for his feedback, which is informing the next stage of development.

Finally, I was a moderator on phpBB forums for many years and understand the problem with disjointed discussions when posts are removed. I don't see any harm in reinstating them but of course I accept the decision of the moderators.

[Alex Kontorovich]

I was unnecessarily harsh, and have edited my message. But your first statement was “A fully verified Lean 4 framework for constructive bounded prime gaps is now live”. There’s nothing wrong (in my book, not others) with using AI for assistance, but the person using it, I believe, is responsible for the outcome before making any claims. Lean is not a panacea and compilation is not a catch-all certificate.

[Bob Jefferson]

@Alex Kontorovich I appreciate your reconsideration. The initial announcement was perhaps poorly phrased; “framework” was intended literally — a verified Lean 4 environment for exploring bounded-gap methods, not a formal proof of the Twin Prime Conjecture.

I want to reiterate that everything released so far is reproducible infrastructure: sieve and averaging machinery, not new theorems, and I am indeed personally responsible for the outcome.

You’re also right that Lean compilation isn’t a guarantee of correctness in itself — that’s why the repo keeps the scope narrow, with a clean façade and an explicit audit of axioms, so others can inspect and extend it safely. My hope has been precisely to attract critical feedback like yours before any formal submission.

I'm currently running a timestamped clean rebuild and will post the results when it finishes in an hour or so but what I really need of course is independent verification, which is the entire point of the exercise.

[Bob Jefferson]

As promised:

Algorithm : SHA256
Hash : D87269FDD1F57D4911927B4F188252AE493A62A7D88B8ACFC4123249E61AC48A
Path : C:\Projects\zenodo-min\lake-manifest.json

PS C:\Projects\zenodo-min> # 3) Clean build artifacts, then run the four verified targets
PS C:\Projects\zenodo-min> Write-Host "`n=== Clean ==="

=== Clean ===
PS C:\Projects\zenodo-min> lake clean

PS C:\Projects\zenodo-min> Write-Host "`n=== Build: Sieve.Analytic.RunAll ==="

=== Build: Sieve.Analytic.RunAll ===
PS C:\Projects\zenodo-min> lake build Sieve.Analytic.RunAll
Build completed successfully.
PS C:\Projects\zenodo-min> Write-Host "`n=== Build: Sieve.Examples.TwinFromAvg ==="

=== Build: Sieve.Examples.TwinFromAvg ===
PS C:\Projects\zenodo-min> lake build Sieve.Examples.TwinFromAvg
Build completed successfully.
PS C:\Projects\zenodo-min> Write-Host "`n=== Build: Sieve.Examples.Gap600FromBVLite ==="

=== Build: Sieve.Examples.Gap600FromBVLite ===
PS C:\Projects\zenodo-min> lake build Sieve.Examples.Gap600FromBVLite
Build completed successfully.
PS C:\Projects\zenodo-min> Write-Host "`n=== Build: Sieve.Audit.Axioms ==="

=== Build: Sieve.Audit.Axioms ===
PS C:\Projects\zenodo-min> lake build Sieve.Audit.Axioms

PS C:\Projects\zenodo-min> Write-Host "`n=== Completed all verified build targets ==="

=== Completed all verified build targets ===
PS C:\Projects\zenodo-min> Get-Date

12 October 2025 15:03:59

PS C:\Projects\zenodo-min> # 4) End transcript and print where the log is
PS C:\Projects\zenodo-min> Stop-Transcript | Out-Null

---

PowerShell transcript end
End time: 20251012150359

I also have a screen recording of the last minute or so of the build.

[Bob Jefferson]

For completeness:

--- Versions ---
Lean (version 4.22.0-rc4, x86_64-w64-windows-gnu, commit 30ceb3260d7d7536092fedff969b4b2e8de7f942, Release)
Lake version 5.0.0-src+30ceb32 (Lean version 4.22.0-rc4)
Microsoft Windows 10.0.26200

=== Re-run Axioms ===
Ôä╣ [6998/6998] Replayed Sieve.Audit.Axioms
info: Sieve/Audit/Axioms.lean:18:0: 'Sieve.Analytic.fraction_ge_threshold_of_avg_with' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Sieve/Audit/Axioms.lean:21:0: 'Sieve.Analytic.Windows.primes_gap_le_of_two_hits' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Sieve/Audit/Axioms.lean:24:0: 'Sieve.Analytic.RunAll.BoundedGapFromTwoHits' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Sieve/Audit/Axioms.lean:25:0: 'Sieve.Analytic.RunAll.BoundedGapFromBoundedWindow' depends on axioms: [propext, Classical.choice, Quot.sound]
Build completed successfully.
ExitCode: 0

12 October 2025 15:14:40

[Yaël Dillies]

Bob, your original message misrepresented the situation: Had you from the start used your own voice (I see that the past few messages were not AI-written, thank you for that) and disclaimed the use of AI, people like Harald and Terry would have engaged with you (or not) in full knowledge of the fact, and I would have been much easier on you. You must understand that with the recent advent of LLMs, not a day passes without someone trying to pass their LLM output on this Zulip as genuine breakthrough or whatnot.

[Yaël Dillies]

There will soon be clearer guidelines relating to the use (and disclosure thereof) of AI. I hope that you can enjoy our welcoming community for what it is, a gathering of human experts ready to help beginners with a genuine intention to learn, and this without compromising its quality and integrity by posting further unacknowledged AI-generated content.

[Bob Jefferson]

Yaël, I do understand and I offer my sincere apologies to anyone who feels that they have been deceived. I'm happy to acknowledge and give credit for the AI assistance I have in this project but I felt that to be open about it at the outset would mean that I wouldn't be taken seriously due to the amount of prejudice (much of it understandable) towards AI. I am very much aware of both its current strengths and weaknesses and through painful trial and error have established a way of using it to best effect.

We are making good progress but I'm very much aware that there is a limit to what I can do alone (even with AI assistance) and I will be relying very much on this community to steer me in the right direction and to tell me when I've got it wrong. I genuinely hope to make a contribution, however small, in this field and I am very grateful to anyone who is willing to help in any way. More than anything right now, I just need independent verification that the scripts run successfully on the latest release.

[Yaël Dillies]

Bob Jefferson said:

I felt that to be open about it at the outset would mean that I wouldn't be taken seriously due to the amount of prejudice (much of it understandable) towards AI

In this community, it is the opposite :slight_smile: Here is a recent example of a good use of AI: #mathlib4 > Problem on possibility of Chebyshev Polynomial @ 💬

[Yaël Dillies]

Bob Jefferson said:

I genuinely hope to make a contribution, however small, in this field

It looks to me that what happened with your project above is that you wrote some statement which you believed encapsulates some truth about prime gaps, but is essentially vacuous. Here's my suggestion to you: Do not state theorems yourself, instead only prove theorems that have been stated by an expert (preferrably a Lean expert, but hopefully a maths expert would do a reasonably good job too).

[Yaël Dillies]

In this case, it looks like you already got some initial informal guidance from Arend above in the thread. I suggest you push your questions further until you get a formal statement out. Then do whatever you want with AI or whatnot, so long as that formal statement doesn't change

[Yaël Dillies]

Warning: Proving such a formal statement is expected to be much harder than for your previous (vacuous) statement.

[Bob Jefferson]

@Yaël Dillies I've been at pains to explain that what I'm building is architecture. I'm happy to leave the theorems to the experts. The next version (v1.3) will extend the framework to include an analytic bridge and future work will focus on analytic interfaces. I hope the slightly revised description for the next release makes this clear:

A Constructive Lean 4 Framework for Bounded Prime Gaps

This archive provides a complete, reproducible Lean 4.22.0-rc4 formalization of a modular scaffold for constructive reasoning about bounded prime gaps.

The framework implements a verified Selberg-sieve–style architecture in three layers:
• Constructive core — a predicate-parametric mass-distribution inequality (fraction_ge_threshold_of_avg_with);
• Stage 3 bridge — an analytic-provider abstraction linking real-valued inequalities to integer-level consequences (fraction_heavy_ge_t_of_AI);
• Combinatorial layer — a window→gap lemma ensuring bounded prime-gap instances under general conditions.
Example façades: the twin-window (gap = 2) and bounded-gap ≤ 600 cases.

All proofs compile with no sorry, depend only on standard mathlib axioms (propext, Classical.choice, Quot.sound), and are verified under a pinned toolchain and mathlib commit.

The accompanying PDF paper documents the architecture, module hierarchy, and the translation from classical analytic reasoning into constructive Lean formalization.
No new mathematical theorems are claimed.
The emphasis is on formal verification, reproducibility, and clarity of design for future bounded-gap formalizations.

In the end, the project will stand or fall on its own merits. I expect the work to be difficult and time-consuming so it's fortunate that I have lots of time, unlimited patience and an obsessive nature. I welcome assistance from anyone along the way, whether human or AI.

[Kevin Buzzard]

Bob, this is low-effort work which anyone could do with a language model. I cannot imagine who you think you are helping here; Lean experts also have access to language models. Low-effort posts posting AI-generated code like this are violations of the community guidelines for this forum. Please refrain from posting any further about your work on this forum.

[Michael Rothgang]

I cannot imagine who you think you are helping here

That's a fairly strong wording. Let's not try to prescribe other's intentions here.

[Michael Rothgang]

For the record, I agree with the main part of the message: while I see your good intentions, I don't think this is actually useful for others. On the other hand, it has a negative effect (such as taking other people's time). Please refrain from posting such low-effort posts in the future.

[Kevin Buzzard]

Michael Rothgang said:

I cannot imagine who you think you are helping here

That's a fairly strong wording. Let's not try to prescribe other's intentions here.

Fair enough Michael. Bob I'm sorry if this part of my message was over the top. But the general sentiment remains.

[Harald Helfgott]

Well, technically, Kevin was assuming that someone here was trying to help others, but that's hardly a noxious assumption, though it may be unwarranted.

[Michael Rothgang]

I read the part I quoted as "you don't even think you're helping anybody", and I've yet to see a discussion where such a statement would be helpful. I don't have any objections to your interpretation :-)

[Harald Helfgott]

I read it as "I assume good faith, hence I assume you believe you are helping someone - I just cannot fathom whom".

[Michael Rothgang]

Ah, that makes much more sense!