Miniproject: prove that li(x)=Li(x)+li(2) and li(2)~ 1.0451

Stream: PrimeNumberTheorem+

[Terence Tao]

A deceptively simple miniproject has shown up as part of IEANTN, PNT#758 PNT#759: to show that the two logarithmic integrals $\mathrm{li}(x) = \int_0^x \frac{dt}{\log t}$, $\mathrm{Li}(x) = \int_2^x \frac{dt}{\log t}$ are related by $\mathrm{li}(x) = \mathrm{Li}(x) + \mathrm{li}(2)$ for $x \geq 2$, and furthermore that $\mathrm{li}(2)$ (also known as the Ramanujan-Soldner constant is approximately 1.0451).

Looks easy, no? But there is a major wrinkle: the integral $\int_0^x \frac{dt}{\log t}$ is not absolutely integrable due to a singularity at $t=1$, and must be defined in a principal value sense. Currently I am defining $\mathrm{li}(x)$ as the rather horrible

noncomputable def li (x : ℝ) : ℝ := lim ((𝓝[>] (0 : ℝ)).map (fun ε ↦ ∫ t in Set.diff (Set.Ioc 0 x) (Set.Ioo (1-ε) (1+ε)), 1 / log t))

Because of this, standard Mathlib integration lemmas do not apply, and some actual mathematical thought has to go into proving these lemmas.

Probably what needs to be done is to find some alternate expression of $\mathrm{li}(x)$ that is not a principal value integral, prove the required results for that expression, and then find some way to connect that expression to the original definition. One possibility is to first show that $\mathrm{li}(x) = \mathrm{Ei}(\log x)$ where $\mathrm{Ei}$ is the exponential integral function, and develop enough of the theory of the exponential integral to finish the job. As far as I can tell this has not yet been done in Mathlib. Anyone have any suggestions on how best to proceed here?

[Kevin Buzzard]

Why not define it as Li(x)+1.0451? Presumably you want to think about that integral near 1 as little as possible?

[Terence Tao]

Well, if the two theorems in PNT#758 PNT#759 are proven, then effectively we do have $\mathrm{li}(x) = \mathrm{Li}(x) + 1.0451$ so the rest of the project should proceed, except possibly in some edge cases when formalizing a statement involving $\mathrm{li}(x)$ that really did use the original definition of $\mathrm{li}$. But I think this miniproject could be a warmup for other numerical integration tasks that we will inevitably face later.

In any case I think I have a reasonable way to approach the problem. One first proves some bounds of the form $\log(1+t) = t + O(t^2)$ for small $t$, which can be used to make $|\frac{1}{\log (1+t)} + \frac{1}{\log(1-t)}| \leq \frac{1}{2(1-t/2)^2}$ bounded for small $t$, which is enough of a bound to allow one to replace the principal value integral with an absolutely convergent integral, e.g., replacing $\int_0^2 \frac{dt}{\log t}$ with $\int_0^1 (\frac{1}{\log(1+t)} + \frac{1}{\log(1-t)})\ dt$. This should then be numerically computable to be about $1.0451$. I'll update the PRs soon to implement this.

[Terence Tao]

added PNT#764 PNT#765 PNT#766 PNT#767 PNT#768 to execute this plan (making the previous two tasks significantly smaller in difficulty).

[Alejandro Radisic]

@Terence Tao

Happy to discuss here about the prove li(2) bounds PR

Looking at the open issues, there's a recurring pattern, integral bounds, log bounds, numerical approximations (#759, #765-768, various FKS2/BKLNW-APP lemmas)

LeanCert provides infrastructure for all of this: certified integration, interval arithmetic, Taylor models. One dependency, many issues. No FFI, no unsafe, no additional toolchain.

What concerns should I address to make this work?

[Terence Tao]

Thanks for the contribution! I am not familiar with LeanCert, but it does sound like a useful set of tools for this sort of project. But I am wondering at a technical level how adding LeanCert as an import would work. With the setup in your current PR, a chunk of the verification of $\mathrm{li}(2)$ would not be hosted in the main PNT+ repository, but instead at the LeanCert repository, and in particular would be beyond the visibility of the blueprint structure we have here. This makes it more difficult to maintain the code; for instance, if at some point we wish to improve the current bounds $1.039 \leq \mathrm{li}(2) \leq 1.06$ to something sharper, this could not be done within the current blueprint system. (But the current bounds may be sufficient for most applications; we shall see.)

Perhaps if one integrated the proof more with the current blueprint at https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/secondary-chapter.html#a0000000037 and went through the more usual workflows of claiming issues, and submitting PRs that modify the existing Lean files (in this case, SecondaryDefinitions.lean), rather than having them in separate files, some of which are hosted outside of PNT+? The LeanCert approach differs slightly from the blueprint one so one may need to modify the blueprint accordingly if doing so.

The other concern I have is whether adding LeanCert as an inport (through changing the lake manifest and lakefile) introduces any challenges with keeping the repository updated with the latest version of Mathlib, or whether it will introduce any issues for contributors who are working with local forks of the repository. In a previous project (EquationalTheories) we eventually decided not to use any imports (such as Duper) that did not come bundled by default with the standard installation of Lean+Mathlib, in order to avoid these issues. But I know very little about how maintainability of imports actually works, so would be interested to get some informed opinions on this.

[Alejandro Radisic]

These are fair concerns. Let me address them:

Blueprint integration: I can restructure the PR so the li(2) proof lives entirely in SecondaryDefinitions.lean, using LeanCert only as numerical infrastructure. Concretely, the bounds theorem would look like:

  theorem li_two_lower : (1039 : ℚ) / 1000 ≤ li 2 := by
    rw [li_eq_symmetric_integral]
    interval_integrate 3000

with the numerical integration certificate and precision parameters living in PNT+ code, fully visible in the blueprint and modifiable by the team. Tightening the bounds later would simply amount to adjusting constants or the partition count in this file.

LeanCert would provide the verified numerics engine, while PNT+ would own the actual theorem and its statement.

Mathlib tracking: LeanCert already tracks Mathlib; I recently updated it to accommodate recent API changes and am committed to maintaining compatibility going forward. If external dependencies are still a concern, a fallback option would be to vendor only the minimal numerical components needed here (interval arithmetic and Taylor models), though I would prefer to avoid that unless necessary.

Workflow: I’m happy to claim the relevant issues and submit PRs that modify the existing files following the standard blueprint workflow. I can do this quickly so as not to block other claims.

Would this “LeanCert as engine, proof in PNT+” structure be sufficient to address the maintainability concerns you raised?

Disclaimer: LeanCert is a tool of my own creation.

[Terence Tao]

Thanks, that does address most of my concerns. The remaining issue is how adding LeanCert as an import will affect the user experience of contributors working with local versions of the repository. If the impact on users is similar to that of a mathlib bump, this would not be a problem thanks to the ability to build mathlib from a cache, but if each user has to build all of LeanCert from scratch this might become an issue, especially if LeanCert is frequently updated. How lightweight is this package and will there be noticeable effects on the user side of including it as an import?

[Ruben Van de Velde]

Looks like leancert depends on mathlib, so we'd only be able to update mathlib when leancert has done so first, and there'd be no cache for it

[Terence Tao]

Oh, so we'd have to either stop updating mathlib, or else have every user rebuild mathlib (and LeanCert) from scratch every time we bump? Neither option sounds all that good to me.

[Alex J. Best]

The mathlib cache would always work in this setup I belive (so no recompiling mathlib). And if LeanCert were to adopt https://github.com/leanprover-community/mathlib-update-action (and had a small chance of breaking) then you could likely rest assured that bumping leancert to latest would bump mathlib to near latest

[Alejandro Radisic]

Thanks Alex for the pointer! I'll adopt mathlib-update-action to keep LeanCert tracking Mathlib automatically.

On build time: a clean build of LeanCert takes about 2.5 minutes on a modern machine (M4 Max, with Mathlib cached). The core modules PNT+ would use compile faster still. I can set up a cloud cache for LeanCert oleans if desired, though at 2.5 minutes it may not be necessary.

Happy to proceed with the PR once these concerns are addressed

[Terence Tao]

If mathlib bumping and cacheing works as before and the only additional overhead is 2.5 mins of build time per LeanCert update, and if one can revert back to the previous setup in case the update process encounters technical issues, then I would tentatively be willing to experiment with this. (But if we started having multiple imports like this, these additional 2.5 mins could start adding up, given that one presumably would have to do this with each Mathlib bump...)

[Ruben Van de Velde]

And also every time you switch branches across a bump, though perhaps that's not too oftern

[Terence Tao]

If LeanCert can handle all the other verified integration/summation tasks that we will likely encounter in this project, it may be a good investment in the long run.

[Alejandro Radisic]

Updated the PR with full integrability and substitution proofs, the li(2) bounds are now proven end-to-end via LeanCert's interval arithmetic

I see PNT#765 - PNT#767 (log bounds) were independently proven while I was working, great to see the activity! This actually clarifies LeanCert's niche: numerical integration where pure calculus can't reach

What's done:

• li2_symmetric_lower/upper: 1.039 ≤ li(2) ≤ 1.06
• g_intervalIntegrable_full: integrability of the symmetric form
• limit_integral_g: ∫_ε^1 g → ∫_0^1 g as ε → 0⁺
• mathlib-update-action adopted

One sorry remains: li2_symmetric_eq_li2 (connecting PNT+'s lim-based li definition to the symmetric form) - this is definition compatibility, not a mathematical gap.

If this works out, happy to help with similar numerical bounds elsewhere in the project

[Pietro Monticone]

Thank you, Alejandro!

Quick note: #ISSUE_NUMBER refers to a Mathlib issue number. For this project, please use the PNT#ISSUE_NUMBER (e.g. PNT#765).

[Kim Morrison]

(Bystander: I think LeanCert is cool, and I hope you guys will stress test it. If it works well, we can take interval arithmetic off the FRO roadmap. If it doesn't, we'll know more about what we're aiming for. Relatedly, we very much feel your pain regarding adding imports with uncached oleans, and the FRO (particularly Mac) is working hard to have a good solution to this; hopefully this quarter.)

[Terence Tao]

OK, I think it's worth experimenting with this tool, so @Alejandro Radisic , if you can go ahead and refactor the contribution as indicated above, aligning with the current blueprint when it makes sense to do so, and update SecondaryDefinitions.lean with suitable imports to fill in the sorry in (a weaker form of) li.two_approx (except for li2_symmetric_eq_li2, which for organizational purposes should probably be placed also in SecondaryDefinitions.lean to make it visible to the blueprint). The Li2Bounds.lean file can still be kept as a standalone import, which will hopefully stay stable and not need to be rebuilt as the rest of the project evolves (so we don't need to do any expensive numerical integration of li(2) over and over again). The remaining sorry I can then make a fresh task for.

Also, if you can use the claim system to claim the specific issues you will be filling in, that would be great (though it seems that PNT#759 has already somehow figured out that PNT#774 will be solving it.

[Alejandro Radisic]

Thanks! I'll refactor as requested

Also about to finish the li2_symmetric_eq_li2 proof

PR coming shortly!

[Lawrence Wu (llllvvuu)]

note that it does use native_decide AFAICT

[Alejandro Radisic]

Thanks @Terence Tao ! Refactored as requested.

• Li2Bounds.lean is now self-contained (stable, won't need rebuilds)
• SecondaryDefinitions.lean imports it
• li2_symmetric_eq_li2 is now in SecondaryDefinitions (blueprint visible)
• li.two_approx_weak sorry is filled (bounds [1.039, 1.06])

PR PNT#774 updated

[Kim Morrison]

Kim Morrison said:

(Bystander: I think LeanCert is cool, and I hope you guys will stress test it. If it works well, we can take interval arithmetic off the FRO roadmap. If it doesn't, we'll know more about what we're aiming for. Relatedly, we very much feel your pain regarding adding imports with uncached oleans, and the FRO (particularly Mac) is working hard to have a good solution to this; hopefully this quarter.)

Oh --- LeanCert does not have a free licence, so I would update my suggestion and discourage use for now.

[Alejandro Radisic]

@Kim Morrison Updated to Apache 2.0. LeanCert is now fully open source.

[Alastair Irving]

A couple thoughts on this:

1. Are we OK with the use of native_decide in LeanCert? Its probably unavoidable for large numerical integrations but the Mathlib docs say "it is probably possible to prove False using native_decide".
2. Could we avoid numerical integration by relating to the exponential integral which has a Taylor series which converges rapidly. The constant term includes Euler gamma so potentially we've just reduced the problem to estimating gamma but that might be independenly useful.

Since PNT#774 is close to being done maybe we should take that for now but consider a Taylor series version without native_decide in the long-term.

[Terence Tao]

1. For this project I think some reliance on external calculations, either through native_decide or simply importing a large calculation as an axiom is unavoidable. The most extreme example of this I have in mind is the numerical verification of the Riemann hypothesis up to some large height H (e.g., H = 10^18), which often require massive amounts of CPU that would beyond the range of even native_decide. But as long as these computations can also be verified by non-rigorous means (e.g., using numpy, pari, SAGE, etc.) I think the risk of catastrophic error is very low, especially if we use somewhat generous safety margins for the accuracy of our numerics, e.g., only estimating li 2 to two decimal places.
2. This could be an interesting side project. One could even imagine setting up a competition to "golf" the estimation of li 2 to a given amount of precision using as few heartbeats or CPU as possible. And having some support in Mathlib for both the logarithmic integral and exponential integral (maybe focusing more on theoretical results such as li x = Ei (log x)) could be worthwhile even outside of PNT+.

[Kevin Buzzard]

I think that there are a bunch of people out there who would be very interested in formal numerical computations in Lean, and rather than just assuming things you might want to put questions out as challenge problems to the wider community as well. There are two levels: proof with native_decide and proof without, and there are definitely people out there who can do all sorts of surprising calculations in Lean who might take the bait. Many years ago I asked how far Lean was able to verify binary Goldbach (motivated at least in part by Harald's work, which needs a nontrivial input here) but this was just when Lean 4 was starting and nobody took the bait. I think the main problem at the time was that we basically had no maths library at all in Lean 4 and hence no reasonable way to prove that a number was prime other than trial division.

[Alejandro Radisic]

This resonates with one of the reasons I built LeanCert, there's a gap between "theoretically computable" and "practically verifiable" for numerical bounds, and I wanted infrastructure to bridge it.

On native_decide: LeanCert uses it in the interval arithmetic kernel for performance. The architecture separates the expression language and correctness theorems from the evaluation kernel, but practically speaking, native_decide is what makes verified numerics feasible at scale. I believe eliminating it would require manual proofs that explode in size, though I'd be curious if others see a cleaner path.

If folks want to set up challenge problems around numerical verification, happy to provide LeanCert as a baseline to beat.

If PNT#774 lands, happy to tackle more numerical bounds elsewhere in the project :grinning_face_with_smiling_eyes:

[Harald Helfgott]

What I've heard said by experts is that large, numerically intensive computations (such as verifying RH up to 10^12, to give a height that has been reached by "rigorous" computation, meaning carefully implemented interval arithmetic) could and ought to be verified by means other than Lean - such as their being performed by code that has been proved to be correct (by Rocq perhaps?) or in a formalizing environment that has been optimized for rapid computation (not sure whether Metamath was mentioned as an example of the latter or the former).

[Harald Helfgott]

And, since Kevin mentioned it: the non-trivial computational input to ternary Goldbach is the verification of GRH up to a certain height and conductor (Platt, interval arithmetic) - I think verifying binary Goldbach up to 10^14 or 10^15 should be fairly small potatoes by now (right?) and that should suffice.

[Alejandro Radisic]

@Harald Helfgott Thanks, that perspective actually aligns very closely with what motivated LeanCert in the first place.

My long-term interest is things like tightening upper bounds for the de Bruijn–Newman constant; Polymath15 (especially the Λ ≥ 0 lower bound work) was a big inspiration. What struck me there was the gap between numerically rigorous computations and formally checkable statements that can be reused downstream.

I agree that Lean itself is probably not the right environment to perform extremely heavy computations like RH verification at large heights. The way I’m thinking about LeanCert is more as infrastructure for certified bounds and compositional reasoning: once a numerical bound has been established by trusted interval arithmetic code (or another optimized system), Lean can be used to integrate that bound cleanly into a larger formal argument without redoing the computation.

In that sense, LeanCert is not meant to replace external numerics, but to make the interface between “rigorous computation” and “formal proof” less brittle. Whether that interface should ultimately live in Lean, Rocq, or elsewhere is still very much an open question to me. This is just a first step in exploring what’s possible.