LeanCert

Certified numerics for Lean 4.

LeanCert turns numerical certificates into theorems about real-valued expressions. Its leancert tactic handles point inequalities, quantified bounds on boxes and natural-number tails, root existence and uniqueness, global bounds, finite sums, and definite integrals. Imported downstream functions can participate through checked enclosure rules without being added to LeanCert's internal expression language. The library also exposes the checked interval, optimization, root-finding, and integration APIs underneath the tactic.

Five proofs

import LeanCert.Tactic

-- A transcendental constant inequality.
example : Real.log 2 < 7 / 10 := by
  leancert

-- One proof covers every real x in the interval.
example : ∀ x ∈ Set.Icc (0 : ℝ) 1,
    Real.exp x * Real.cos x ≤ 3 := by
  leancert

-- Existence and uniqueness, certified by interval and Newton arguments.
example : ∃! x, x ∈ Set.Icc (1 : ℝ) 2 ∧ x ^ 2 - 2 = 0 := by
  leancert

-- Polynomial integrals are normalized and checked exactly over ℚ.
example : (∫ x in (0 : ℝ)..1, x ^ 2) = 1 / 3 := by
  leancert

-- LeanCert discovers and certifies a cutoff for this infinite tail.
example : ∃ N : Nat, ∀ n ≥ N, (3 : ℝ) / n ^ 2 ≤ 1 / 1000 := by
  leancert

These are ordinary Lean theorems, not tests against sampled floating-point values. The exact snippets above are compiled in CI.

Install and prove something

LeanCert currently tracks the Lean and Mathlib versions in lean-toolchain and lakefile.toml. Add it to a Lake project:

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

Then update dependencies:

lake update

Create Main.lean:

import LeanCert.Tactic

example : Real.exp 1 < 3 := by
  leancert

Check it with:

lake env lean Main.lean

For a reproducible development or release, pin rev to a commit or tag rather than main.

Prefer Python?

The self-contained Python SDK bundles the matching LeanCert Bridge on supported platforms, so checking a claim does not require a local Lean installation:

pip install leancert
leancert doctor

import leancert as lc
from leancert import ast

x = ast.var("x")
result = lc.prove(x**2 <= 1, where={x: (0, 1)})

if isinstance(result, lc.Verified):
    print(result.claim_id)

Python handles exact modeling and untrusted candidate search; advertised LeanCert checkers authorize successful outcomes. Replayable results can be exported as pinned Lean projects for an independent kernel rebuild. Begin with the Python SDK documentation.

What is actually verified?

LeanCert separates finding a certificate, checking it, and interpreting it.

 goal in Lean
      │
      ▼
 reify expression ──► search for interval/root/integral certificate
                              │
                              │  untrusted candidate data
                              ▼
                    executable certificate checker
                              │
                              │  proof that check = true
                              ▼
                  proved soundness / “golden” theorem
                              │
                              ▼
                       theorem in Lean

Search, heuristics, and candidate generation do not need to be trusted: a bad candidate fails the checker. The checker is connected to the mathematical claim by proved soundness theorems. CI audits the production golden theorems for dependencies beyond Lean/Mathlib's standard foundations.

There are two ways to prove the closed proposition check = true:

Choose the route per proof:

import LeanCert.Tactic

example : Real.log 2 < 7 / 10 := by
  leancert (trust := kernel)

Or set it for a section or file with set_option leancert.trust "kernel". Numerical backend selection (Rational/Dyadic/Affine) is independent of this verification choice.

See the authoritative trust model and the compiled curated showcase.

Why not norm_num, positivity, or a basic interval tactic?

These tools are complementary:

LeanCert itself uses ordinary algebraic automation for side conditions. Its distinctive role is proof-producing numerical search plus a checked certificate bridge to the final proposition. Run leancert? when you want to see which dedicated solver the router selected.

What is in the library?

The main verified numerical path includes:

• Rational, Dyadic, and Affine interval evaluation
• Algebraic operations and supported transcendental functions including exp, log, sin, cos, sqrt, atan, atanh, and erf
• Checked automatic differentiation and global bound certificates
• Root existence, exclusion, Newton-style uniqueness, and automatic or manual Krawczyk system-root certificates
• Exact rational polynomial integration and certified partition integration
• Checked downstream unary enclosure rules consumed compositionally by leancert or the lightweight enclosure_bound front door
• Fixed and automatically discovered reciprocal-power bounds over infinite natural-number tails
• Domain-specific Chebyshev, analytic-number-theory, q-product, table, and neural-network certificate infrastructure

For programmatic use, start with the stable LeanCert APIs:

• LeanCert.evalInterval and LeanCert.evalInterval_correct
• LeanCert.API.Bounds
• LeanCert.API.Optimization
• the checked AD, root, and integration APIs described in the documentation

Limitations

LeanCert provides sound automation for a supported fragment; it is not a complete decision procedure for real analysis. A failed or inconclusive search does not imply that the theorem is false.

• Tight bounds can require greater Taylor depth, subdivision, or a dedicated optimization tactic, and may still remain inconclusive.
• Sign-change certificates miss even-multiplicity roots, while Newton uniqueness requires additional certified hypotheses.
• Exact integral equalities are automated for rational polynomials; other supported integrands generally use certified partition bounds.
• Supported evaluators may require domain certificates, such as positivity for logarithms or exclusion of zero from denominator intervals.
• Downstream enclosure execution currently targets unary interval bounds. Existing core operations may surround proof-carrying registered subterms; rejected or inconclusive candidates are retried on rational bisections. Unsupported custom operations are not yet covered.
• Eventual-bound automation currently targets nonnegative rational multiples of reciprocal powers over Nat; general logarithmic, exponential, and AD-derived tail rules are not yet supported.

Native verification is faster but additionally trusts Lean's compiler/runtime; kernel-only verification may be substantially more expensive. See the trust model and verification status for precise trust boundaries, experimental subsystem qualifications, and the Li₂ lightweight verification boundary.

See Choosing Tactics and Troubleshooting for the full support matrix and practical guidance.

Repository promises

CI is split into six reviewable guarantees:

The exact commands and scope of each tier are documented in CI Promises.

The visible source layout follows the same ownership model: stable checked entry points live in LeanCert/API, reusable numerical theorems in LeanCert/CertifiedBounds, automation in LeanCert/Tactic, supported demonstrations in LeanCert/Examples, and regressions in LeanCert/Test. See the contributor architecture guide and roadmap for current boundaries and convergence work.

Releases and citation

Archived releases are available from Zenodo:

• v4.32.2.1: 10.5281/zenodo.21681348
• v4.32.1: 10.5281/zenodo.21633981

When citing LeanCert, use the DOI for the exact version used in the proof development.

License

Apache 2.0. See LICENSE.