LeanCert imported

Stream: PrimeNumberTheorem+

[Terence Tao]

I have now approved PNT#774 to import LeanCert into the project for verified numerical tasks, such as numerical integration. However, we are moving certain computationally intensive LeanCert verifications (such as numerical upper and lower bounds on li 2) outside of the main PNT+ lean files to avoid excessive build times. The initial building of LeanCert may take some time, but hopefully this will only need to be done once per mathlib bump. Please let me know if there are any issues with excessively slow build times, or other issues related to this.

[Yongxi Lin (Aaron)]

It seems like that LeanCert can't really deal with inequalities involving the ceiling function, as shown in my PR: PNT#980. In this PR I want to show the following two inequalities:

import Mathlib

example : ⌈Real.exp 59⌉₊ + 4 ≤ 11325 * 10 ^ 22 := by sorry

example : ⌈Real.exp 60⌉₊ + 4 ≤ 7785131284000000000000000004 := by sorry

These two goals can't be automatically solved by interval_decide, so instead I first proved the following two inequalities:

import Mathlib

example : Real.exp 59 + 4 + 1 ≤ 11325 * 10 ^ 22 := by sorry -- solved by interval_decide

example : Real.exp 60 + 4 + 1 ≤ 7785131284000000000000000004 := by sorry -- solved by interval_decide

This might be something LeanCert could improve. Nevertheless, I am still quite impressed by this one-tactic proof of Real.exp 59 + 4 + 1 ≤ 11325 * 10 ^ 22 produced by LeanCert.

[Alejandro Radisic]

Added Nat.ceil preprocessing in interval_decide: goals like ⌈e⌉₊ + k ≤ n are reduced to a real inequality (e ≤ n - k), then closed via Nat.ceil_le + omega.

So with LeanCert’s tactic import, these should now solve with a single interval_decide.

[Alejandro Radisic]

Summary of changes since the last pinned version:

• Chebyshev psi engine (ChebyshevPsi.lean): certified ψ(N) upper bounds via incremental von Mangoldt accumulation, generalized to arbitrary slopes. All bridge theorems fully proved.
• Dyadic backend optimizations: binary exponentiation, sign-based multiplication, Horner evaluation. Dyadic-first dispatch with inv/log fallback.
• interval_decide Nat.ceil support: handles goals involving ⌈e⌉₊ (used in PNT#980).
• Expression reification: added abs, max, min, rational-exponent rpow.
• Warning fixes contributed by @ajirving.

The general pattern for enumeration-based bounds: define a computable Bool checker, prove a bridge theorem ("if checker returns true, the math holds"), then native_decide runs it at native speed.

The same approach could apply to other numerical verification tasks in the project, if the check is expressible as a decidable Bool computation, LeanCert can likely handle it

[Terence Tao]

There is a certain amount of python code in the LeanCert repository. What precisely is the interaction between Lean and Python in LeanCert? Is there any lean code that externally runs a Python script, for instance?

[Alejandro Radisic]

No Lean code calls Python. The Python SDK is a discovery frontend: explore functions, find bounds, locate extrema interactively (lc.find_bounds(...), lc.verify_bound(...)), then write the actual Lean proof using the constants you found.

The workflow is "explore in Python → prove in Lean." The SDK calls a compiled Lean binary under the hood, none of it is in the import path or proof chain

[Kim Morrison]

I wonder if splitting the repository into a pure lean one, and as downstream one for the python library would help here.

[Alejandro Radisic]

That makes sense, will get it done this week!