LeanCert

LeanCert is a Lean 4 library for certified numerical computation and proof-producing certificate workflows.

LeanCert is organized around proof intent:

Direct automation closes concrete bounds, roots, optimizations, and integral goals over explicit expressions.
Proof templates package reusable certificate strategies such as table checking, main-term/error envelopes, perturbation observers, product-integral identities, and contour-shift bookkeeping.
Domain libraries provide specialized mathematics, especially analytic number theory and q-product certificates, built on top of the templates.
Architecture and trust explains checkers, Golden Theorems, arithmetic backends, and verification status.

What Kind Of Proof Are You Building?

I have...	Go to
A concrete inequality over an interval	Direct Automation → Bounds
A root existence, uniqueness, or no-root claim	Direct Automation → Roots
A global minimum or maximum problem	Direct Automation → Optimization and Discovery
A definite integral bound	Direct Automation → Integration
Generated finite rows to verify	Proof Templates → Table Certificates
A summatory function with a main term and error term	Proof Templates → Asymptotic Envelopes
A real-variable approximation with an error radius	Proof Templates → Pointwise Envelopes
A constant built by perturbing a reusable base object	Proof Templates → ConstantFactory
A finite q-product integral	Proof Templates → Exact Product-Integral Certificates
A contour-shift identity	Proof Templates → Contour Shift
Chebyshev, Abel, Euler-product, Dirichlet, or Mertens certificates	Domain Libraries → Analytic Number Theory
A neural-network or transformer verification problem	ML Verification

import LeanCert.Tactic.IntervalAuto

example : forall x in Set.Icc (0 : Real) 1, Real.sin x <= 1 := by
  certify_bound

Add LeanCert as a Lake dependency:

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

Then run:

lake update

Section	Description
Getting Started	Choose the right proof path before selecting modules
Direct Automation	Tactics and commands for direct numeric goals
Proof Templates	Reusable certificate strategies and proof patterns
Domain Libraries	Domain-specific certificate packages
Architecture and Trust	Why checkers imply theorems, and what is trusted
Reference	Imports, tactics, and certificate API references

This repo is Lean-only. The Python package and bridge release pipeline were moved out of this repo.