Skip to content

Quickstart

This quickstart is Lean-only. It gets you to a direct certified bound first, then previews a proof-template workflow.

1. Add LeanCert

In your lakefile.toml:

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

For a reproducible formal development, replace main with a tested LeanCert release tag. This checkout is pinned to the Lean/Mathlib v4.32.2 toolchain; use main only when intentionally testing unreleased changes.

Then run:

lake update

2. Direct Automation: Prove a Bound

import LeanCert.Tactic

example : ∀ x ∈ Set.Icc (0 : ℝ) 1, Real.exp x ≤ 3 := by
  leancert

3. Direct Automation: Find a Root Existence Proof

import LeanCert.Tactic

example : ∃ x ∈ Set.Icc (1 : ℝ) 2, x ^ 2 = 2 := by
  leancert

4. Use Discovery Commands

import LeanCert.Discovery.Commands

#find_min (fun x => x^2 + Real.sin x) on [-2, 2]
#bounds (fun x => x^3 - x) on [-2, 2]

Discovery commands help estimate constants before writing the final theorem.

5. Domain-specific extensions

Q-product constants and perturbation observers are provided by the separate leancert-qproduct package, rather than by LeanCert itself. See the migration guide.

Notes

  • Start direct inequality proofs with leancert; use certify_bound when you intentionally want the dedicated interval-bound engine or explicit Taylor-depth control.
  • Use discovery commands to estimate constants before writing the final theorem.
  • Use proof templates when the proof has reusable structure: generated rows, main/error envelopes, directed limits, or contour-shift bookkeeping.
  • Use lake exe check-compat to validate Mathlib compatibility in larger projects.