LeanCert - Verified Computation & Interval Arithmetic

Stream: general

[Alejandro Radisic]

Finally hit v1.0! Full verification, no sorry markers in the core.

What it does:

-- Prove bounds on transcendentals
example : ∀ x ∈ Set.Icc 0 1, Real.exp x ≤ 3 := by interval_bound

-- Prove root existence (√2)
example : ∃ x ∈ Set.Icc 1 2, x^2 = 2 := by interval_roots

-- Global optimization
#minimize (fun x => x^2 + Real.sin x) on [-2, 2]

Discovery Mode: Don't have a bound in mind? Branch-and-bound optimization finds tight constants, then auto-generates the formal proof.

Fully verified:

• Interval arithmetic (FTIA) for +, -, *, /, ^
• Transcendentals: exp, sin, cos, sinh, cosh, tanh, atan, arsinh, log
• Taylor remainder bounds (Lagrange form)
• Forward-mode AD
• Global optimization (globalMinimize_lo_correct)
• Root finding: bisection + Newton contraction
• Integration bounds
  Architecture: Certificate-driven — reify to AST, compute with rationals, lift to ℝ via golden theorems. All checked by native_decide.

Also includes a Python SDK for exploration workflows.

https://github.com/alerad/leancert

Feedback, issues, PRs welcome!

[Mirek Olšák]

Finally, interval arithmetics! It sounds great! Just two comments

• I am a bit surprised that sqrt is not a basic function. Does it just work with some default efficient translation? (then I would put it to the examples too)
• As I am aware of some degree of skepticism with native_decide, do you plan to also look into kernel proofs (it could work with decide +kernel but perhaps there is a more optimized way)?

[Bbbbbbbbba]

Could you bump up Mathlib version? Or is there some easy way for me to do that locally?

[Alejandro Radisic]

Thanks!

On sqrt: You're right, it's not a primitive, it's defined as exp(log(x)/2) so we can reuse the verified Taylor series for exp and log without deriving separate error bounds. It works, but it's slower than it should be.

Caveat: the automated tactics (interval_bound etc.) don't support sqrt yet because log isn't in the computable core subset (ExprSupportedCore). So while you can use Expr.sqrt in expressions, you can't currently prove bounds on it with the one-liner tactics. Will be working on adding log/sqrt in these days.

On native_decide: Yeah, valid concern about TCB. The short version: rational arithmetic was killing us with GCD computations in deep Taylor series, so we went with native_decide for speed.

Good news is the switch to dyadic arithmetic (integers + bit shifts, no GCDs) might make kernel proofs viable now. Haven't tested it yet, but decide could plausibly work for smaller problems. Plan is to support both; native_decide when you need speed & kernel proofs when you want minimal TCB

[Mirek Olšák]

Regarding GCD, I thought there could be a more efficient way on operating rational numbers in kernel -- you do not need to know that you are dividing with GCD, only that you are dividing with a common divisor. But might not matter if you switched number representation.

[Alejandro Radisic]

sqrt added :saluting_face:

[Mirek Olšák]

Have I done something wrong? I cloned the repo, created an experimental file with

import LeanBound

example : ∀ x ∈ Set.Icc 0 1, Real.exp x ≤ 3 := by interval_bound

and it failed on

Application type mismatch: In the application
  LeanBound.Numerics.Certificate.verify_upper_bound_Icc (LeanBound.Core.Expr.var 0).exp
    (LeanBound.Numerics.ExprSupportedCore.exp (LeanBound.Numerics.ExprSupportedCore.var 0))
the argument
  LeanBound.Numerics.ExprSupportedCore.exp (LeanBound.Numerics.ExprSupportedCore.var 0)
has type
  LeanBound.ExprSupportedCore (LeanBound.Core.Expr.var 0).exp : Prop
but is expected to have type
  LeanBound.ExprSupported (LeanBound.Core.Expr.var 0).exp : Prop

perhaps I cloned an unstable version?

[Alejandro Radisic]

Feel free to try the latest commit please! Wiil tag new version soon too.

I fixed a bunch of bugs related to that one, and have been testing different things throughout the whole day, finding some more issues and fixing them. It should work as expected now, and the library is in a way more solid state.

Sorry about that!

[Mirek Olšák]

Great, now it works.

[Mirek Olšák]

Is there also a tactic to prove numerical inequality only? Like

example : Real.exp 1 ≤ 3 := by sorry
example : Real.sqrt 2 + Real.sqrt 3 > Real.pi := by sorry

[Alejandro Radisic]

Not yet, interval_bound only handles ∀ x ∈ I, ... form currently :(

a workaround for single-point expressions:

example : Real.exp 1 ≤ 3 := by
    have h : ∀ x ∈ Set.Icc (1:ℝ) 1, Real.exp x ≤ 3 := by interval_bound
    exact h 1 ⟨le_refl 1, le_refl 1⟩

For multi-constant expressions like √2 + √3 > π, there's no direct support yet, will prioritize it, and probably have it ready tomorrow.

Thanks a lot for the feedback!

[Mirek Olšák]

You work with a fixed precision?

example : ∀ x ∈ Set.Icc 0 1, Real.exp x ≤ 2.718282 := by
  interval_bound -- failed

It would be cool if the tactic could figure out the necessary precision, and heuristically optimize it to minimize computation in the proof term.

[Mirek Olšák]

Also, it is a bit silly that the other direction of inequality is not supported

example : ∀ x ∈ Set.Icc 0 1, 3 ≥ Real.exp x := by
  interval_bound -- failed

(Sorry I am throwing feature requests at you so quickly.)

[Alejandro Radisic]

Hey! No, I'm happy with them, keep em coming! haha

Both of these are done:

1. Adaptive precision - the tactic now tries Taylor depths [10, 15, 20, 25, 30] automatically until one works

2. Reversed inequalities - added preprocessing that rewrites ≥ → ≤ and > → < before running

Both examples should work now!

[Cookie Guy]

do you plan to support lebesgue integration?

[Adomas Baliuka]

What are the main differences of this project and its aims with https://github.com/girving/interval ?

[Alejandro Radisic]

Great question @Adomas Baliuka

Disclaimer: Didn't know girving/interval existed until today :sweat_smile: (Also started rebranding from LeanBound to LeanCert yesterday, your question confirms the timing was right!)

From what I've seen, girving/interval focuses on a clean, trusted implementation of conservative interval arithmetic with good approximation typeclasses.

We share the mathematical foundation, but LeanCert has a different philosophy and broader scope.

Philosophy:
Numerical computation is scaffolding; the product is a theorem.

Discovery → Proof:

-- Find minimum, get a proven existential
#minimize (fun x => x^2 + Real.sin x) on [-2, 2]
-- Output: ∃ m, ∀ x, f(x) ≥ m  (with rigorous rational bound)

Bound certification:

-- Transcendentals with Taylor models
theorem exp_bound : ∀ x ∈ Set.Icc 0 1, Real.exp x ≤ 3 := by
  interval_bound 15

-- Or faster with Dyadic arithmetic
theorem fast : ∀ x ∈ Set.Icc 0 1, Real.sin x ≤ 1 := by
  certify_bound

Multivariate:

theorem mv : ∀ x ∈ Set.Icc 0 1, ∀ y ∈ Set.Icc 0 1, x + y ≤ 2 := by
  multivariate_bound

Root existence via IVT

-- Prove √2 exists
theorem sqrt2 : ∃ x ∈ Set.Icc 1 2, x² = 2 := by interval_roots

-- Prove exp(x) has no roots (always positive)
theorem exp_no_root : ∀ x ∈ Set.Icc 0 1, exp(x) ≠ 0 := by root_bound

Architecture: Built around "Golden Theorems" connecting boolean checks to mathematical properties. Multiple backends (exact Rational, fast Dyadic) feed into the same trusted verifier.

Also supports counterexample hunting (interval_refute), neural network verification with affine arithmetic.

Python SDK: LeanCert includes a JSON-RPC bridge for Python integration. Python acts as an untrusted oracle, you can use NumPy/SciPy to explore, find candidate bounds, then send them to Lean for formal verification. The SDK provides a high-level symbolic API (x**2 + sin(x)) that translates automatically, with no de Bruijn indices or Lean AST knowledge needed. Lets anyone compute fast and prove rigorously in the process.

Let me know if this solves your doubt, happy to discuss more!

[Shreyas Srinivas]

How does this compare with Scilean?

[Alejandro Radisic]

Thanks for asking @Shreyas Srinivas

I’m aiming at something different.
SciLean is about doing scientific computing in Lean, while LeanCert is about proving numerical facts.

SciLean treats Lean as a high-level numerical / scientific language: you write models, run simulations, do differentiation, optimization, etc, and you get numerical results

LeanCert treats Lean as a proof checker: you may explore numerically, but the end goal is to turn those insights into formal theorems. The output is proof terms, not floats.

For example:

SciLean:
"Simulate this damped oscillator and plot the response."

LeanCert:
"Prove that the damped response never exceeds 1."

theorem damped_bounded : ∀ t ∈ Set.Icc (0 : ℝ) 5,
    Real.exp (-t) * Real.sin t ≤ 1 := by
  certify_bound

So while SciLean optimizes for expressiveness and performance, LeanCert optimizes for rigor via interval arithmetic and certified bounds.

I think they'll complement nicely, you might use SciLean to model, experiment, and discover invariants, then use LeanCert to formally certify the critical numerical properties you care about.

[Bas Spitters]

Exciting!
How does this relate to the porting effort from Rocq's Floqc library that was discussed a couple of times?
@Jason Gross also expressed plans to try to automatically port flocq.

[Alex Meiburg]

There's also https://github.com/Timeroot/ComputableReal, but I'm very happy that LeanCert seems to completely eclipse that one in scope in several ways. :)

[Notification Bot]

A message was moved here from #announce > LeanCert - Verified Computation & Interval Arithmetic by Floris van Doorn.

[Floris van Doorn]

@Bas Spitters I moved your message to this discussion thread.

[Bjørn Kjos-Hanssen]

Great tool. I was able to use it to formally verify a solution to an actuarial textbook question. The answer in the back of the book was "0.064" whereas the precise answer was

(Real.exp (7 / 144) -  Real.exp (6 / 125)) * 100

Minor suggestion: maybe make this work:

example : (0.9 : ℝ) ≤ 1.08⁻¹ ∧ 1.08⁻¹ ≤ (1:ℝ) := by interval_decide

Right now this works:
constructor;interval_decide (typinginterval_decide only once)

[Alejandro Radisic]

@Bas Spitters

My understanding is that FLOQC is about precise reasoning about floating-point arithmetic itself (IEEE semantics, rounding, ulps, etc), whereas LeanCert is operating at a different layer: it works over ℝ and uses interval arithmetic and Taylor models to certify numerical properties (bounds, roots, optima) as theorems in Lean.

FLOQC-style libraries are ideal when you need to reason about floating-point error in algorithms, while LeanCert is aimed at proving analytic facts and safety bounds without committing to a specific floating-point model

[Alejandro Radisic]

@Bjørn Kjos-Hanssen

Thanks!
Textbook use case, literally! Just pushed a fix, interval_decide should handle conjunctions directly now.

[Bas Spitters]

@Alejandro Radisic you are right, I was trying to say too many things at the same time. There is a porting effort going on for flocq. This made me think of the related work by the same author on coq interval and gappa. https://gappa.gitlabpages.inria.fr/
https://coqinterval.gitlabpages.inria.fr/

[Alejandro Radisic]

@Bas Spitters

Thanks, that makes sense.

Yes, CoqInterval is definitely much closer in spirit. I see LeanCert as exploring a similar analytic layer, but with a different emphasis: certificate-driven automation, and especially "discovery workflows" (optimization, root finding, not just discharging given inequalities).

That being said, I realize I should probably make positioning clearer in the announcement section, and I’ll update that shortly.

From what I've read, Gappa sits lower, closer to implementation-level reasoning, while LeanCert intentionally stays at the ℝ level

So I don’t see this as overlapping with the Flocq porting effort, I think they will actually complement too!

[Bas Spitters]

Yes, gappa sits at a lower level.
From what you write, I don't see a big distinction in approach with coq-interval, but that's probably my limited understanding of LeanCert. So, I look forward to the positioning. In any case, exciting to see this in lean!

[Bjørn Kjos-Hanssen]

Why am I getting this error? :embarrassed: Is it that I have to be on the same Mathlib version as LeanCert is?

error: LeanCert/Core/Taylor.lean:144:32: Application type mismatch: The argument
  h_one_le
has type
  1 ≤ ↑(n + 1)
but is expected to have type
  ↑(n + 1) ≠ 0
in the application
  ContDiff.differentiable hf h_one_le

[Ruben Van de Velde]

Well yes, of course leancert needs to use the version of mathlib that it works with. But lake should handle that. How did you get to this point?

[Bjørn Kjos-Hanssen]

I did something like rm -rf .lake/leancert and then redid lake update leancert, after lake initially complained that leancert "has no branch called master". Maybe that was not the cleanest approach.

[Ruben Van de Velde]

Why are you running lake update and where?

[Alejandro Radisic]

@Bjørn Kjos-Hanssen The default branch is 'main', so that's likely the issue. Your lakefile should have:

[[require]]
name = "leancert"
git = "https://github.com/alerad/leancert"
rev = "main"

Then do a clean rebuild:

rm -rf .lake lake-manifest.json
lake update
lake build

Lake will pull LeanCert along with its pinned Mathlib version (v4.27.0-rc1) and everything should match up.

Curious though, where did you get master from? Just want to make sure there isn't stale documentation floating around somewhere

[Ruben Van de Velde]

I think if you don't put a rev, lake tries master

[Alejandro Radisic]

I will create a master branch that tracks main to avoid these kind of issues...

Thanks @Ruben Van de Velde

[Bjørn Kjos-Hanssen]

Ruben Van de Velde said:

I think if you don't put a rev, lake tries master

Indeed, I didn't put a rev.

Now my only problem is that Warning: some files were not found in the cache. and therefore it will take hours to run lake build.

[Ruben Van de Velde]

That sounds like a setup issue

[Alejandro Radisic]

@Bjørn Kjos-Hanssen

Maybe you need to fetch mathlib cache?

Run lake exe cache get before lake build, that downloads prebuilt Mathlib artifacts. Should take a few minutes instead of hours.

If still gives warnings, maybe:

lake exe cache get! (with the !) to force download it?

Will try to replicate on my side meanwhile

[Bjørn Kjos-Hanssen]

Now I'm back to the original error message about h_one_le even though I added the rev="main".
I guess the error is related to #33131 from last month.
I'll try manually changing my Mathlib version to match yours.

[Kevin Buzzard]

Just to be clear -- your Lakefield doesn't mention mathlib explicitly, right?

[Bjørn Kjos-Hanssen]

What's a Lakefield?

[Bjørn Kjos-Hanssen]

Anyway, it seems to be working now... I just went in to lake-manifest.json and changed the Mathlib version. Now I get instead

stderr:
⚠ [2847/2893] Replayed LeanCert.Engine.Optimization.BoundVerify
warning: LeanCert/Engine/Optimization/BoundVerify.lean:266:13: This simp argument is unused:
globalMaximize

[Alejandro Radisic]

@Kevin Buzzard LeanCert pins Mathlib v4.27.0-rc1, is it a bad call? Also I think adding a separate mathlib requirement breaks it yeah

[Alejandro Radisic]

Does that warn block it from building @Bjørn Kjos-Hanssen ? Should be just a linter warning

[Bjørn Kjos-Hanssen]

My .lean file that actually uses LeanCert builds fine, but then the main project file Interest.lean (that imports the working one) does not.

[Alejandro Radisic]

Does Interest.lean throw any particular error / what error does it throw?

[Bjørn Kjos-Hanssen]

That's the one that says

stderr:
⚠ [2847/2893] Replayed LeanCert.Engine.Optimization.BoundVerify
warning: LeanCert/Engine/Optimization/BoundVerify.lean:266:13: This simp argument is unused:
globalMaximize

[Bjørn Kjos-Hanssen]

(But then again it also has other errors from my own code right now, because my library was using a newer version of Mathilb)

[Alejandro Radisic]

Hmmh, are you canceling early maybe, or is it just stuck there? No build issues so far in that log

[Bjørn Kjos-Hanssen]

It might be that it's failing (in VSCode) because of the other errors and not because of the unused simp argument. I can try to down-version my code and see if that does it.

[Alejandro Radisic]

Can you check that your project's Mathlib version matches LeanCert's (v4.27.0-rc1)? Check your lakefile.toml or lake-manifest.json for the mathlib rev.

[Bjørn Kjos-Hanssen]

Yes I manually set the mathlib rev in lake-manifest.json to 32d24245c7a12ded17325299fd41d412022cd3fe to match LeanCert and it seems to work now.

[Alejandro Radisic]

Awesome, glad it's working! Getting Mathlib versions to align can be... a bit of a dance. lmk if you need help with anything else!

[Bjørn Kjos-Hanssen]

Thanks a lot. I guess whenever you import somebody else's project you have to be careful about the versions. If I import two independent projects (LeanCert and LeanSomeOtherProject) I guess there's no way it will consistently work?

[Bjørn Kjos-Hanssen]

If LeanCert and LeanSomeOtherProject don't coordinate their Mathlib versions?

[Alejandro Radisic]

If both projects pin the same Mathlib version no issues, otherwise... prayer and manual manifest editing

I'm considering adding a small lake run leancert:check-compat or something like that though, I have fought with this many times too haha

[Bjørn Kjos-Hanssen]

If Project1 uses ContDiff.differentiable prior to #33131 and Project2 uses ContDiff.differentiable posterior to #33131 I guess one is out of luck.

[Kevin Buzzard]

Alejandro Radisic said:

Kevin Buzzard LeanCert pins Mathlib v4.27.0-rc1, is it a bad call? Also I think adding a separate mathlib requirement breaks it yeah

Nonono, I was just checking that Bjorn wasn't also requiring (a different version of) Mathlib.

[Kevin Buzzard]

Bjørn Kjos-Hanssen said:

Yes I manually set the mathlib rev in lake-manifest.json to 32d24245c7a12ded17325299fd41d412022cd3fe to match LeanCert and it seems to work now.

Aah OK. Yeah, if you're going to require something then you'd better let lake decide exactly which version of all its dependencies that you're using!

[Bjørn Kjos-Hanssen]

(deleted)

[Bjørn Kjos-Hanssen]

Perhaps it would work to not require Mathlib at all, and instead rely on transitivity since LeanCert requires Mathlib :thinking:

[Ruben Van de Velde]

Yes, please do that

[Ruben Van de Velde]

This is what Kevin meant by "also requiring (a different version of) Mathlib"

[Oscar Matemb ⚛️]

Quick question, can you please clarify the difference between kernel trust ( what lean inherently does) and compiler trust? doesn't lean just rely on its kernel for verification?

[Oscar Matemb ⚛️]

also, I was curious if exploration of bounds for a certain expression can be perhaps done in Lean?

[Henrik Böving]

You can instruct the kernel to trust the result of a program verified in Lean and compiled using leans code generator. This will show up as an additional axiom in the dependencies of your theorem.

[Alejandro Radisic]

@Oscar Matemb ⚛️

Yes, Exploration (Discovery) is supported!

Although I'd recommend giving the Python SDK some love for discovery , recently added witness support that returns the actual point where min/max is achieved, not just the bound (beta)

Find bounds

x = lc.var('x')
expr = x**2 + lc.sin(x)

result = lc.find_bounds(expr, {'x': (-2, 2)})
print(f"min ∈ {result.min_bound}")  # Interval[-0.23..., 0]
print(f"max ∈ {result.max_bound}")  # Interval[4.9..., 5]

Output:
  min ∈ [-5.0000, -0.2325]
  max ∈ [4.9093, 5.0000]
  f(x) ≥ -0.25 verified: True

Verify a specific bound

verified = lc.verify_bound(expr, {'x': (-2, 2)}, lower=-0.25)
print(f"f(x) ≥ -0.25 verified: {verified}")  # True

Output:
  argmin ≈ {'x': -0.4501953125}

[Alejandro Radisic]

Quick update: pip package now standalone

The Python SDK mentioned earlier is now a proper standalone pip package:

pip install leancert

import leancert as lc
x = lc.var('x')
bounds = lc.find_bounds(lc.sin(x) / x, {'x': (0.1, 1.0)}) # Proven, Lean verified

Bundles the Lean4 verification engine (~70MB), no Lean installation or knowledge needed. Works on macOS/Linux/Windows.

This is part of a larger effort to bridge formal verification to broader audiences, making Lean's rigor accessible to people who need provably correct numerics but aren't going to learn a theorem prover.