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:

Mode	Certificate check	Trust added by the generated proof
`native` (default)	`native_decide`	Lean kernel plus compiler/runtime
`kernel`	`decide +kernel`	Lean kernel only; never falls back
`auto`	kernel first, native when gated or unsuccessful	Reports native fallback

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:

Tool	Best at	What LeanCert adds
`norm_num`	Exact normalization of concrete algebraic/numeric goals	Certified enclosures for transcendental expressions and quantified real domains
`positivity`	Deriving that an expression is nonnegative or positive	Quantitative upper/lower bounds, not just a sign
Basic interval tactics	Propagating enclosures through a supported expression	A semantic front door spanning bounds, subdivision/optimization, roots, sums, and integrals

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:

Tier	Status	What it establishes
Core		Stable library, public APIs, and downstream contracts
Functional		Every wired regression and executable smoke test
Docs		README/docs Lean snippets and strict MkDocs build
Soundness		Axiom, `sorry`, proof-hole, and trust-manifest audits
Showcase		Published success and failure demonstrations
Heavy		Expensive certificate targets and benchmark smoke

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.

LeanCert0.1.0