Search + Certify APIs

This module provides high-level APIs that wrap existing numerical algorithms to return answers with proofs, not just verdicts.

These APIs bridge the gap between "verify a guess" and "find the answer":

• findRoots finds isolating intervals with existence proofs
• findUniqueRoot finds a unique root with existence AND uniqueness proofs
• findGlobalMin / findGlobalMax finds extrema with bound proofs
• findIntegral computes integral bounds with correctness proofs

Usage

These APIs are designed to be:

1. Called programmatically from other Lean code
2. Used by the Python SDK to generate certificates
3. Invoked by discovery tactics

Design Philosophy

Each API wraps existing algorithms (bisection, Newton, branch-and-bound, etc.) and bundles the result with the appropriate correctness proof.

Root Finding API (0.1.1)

structure LeanCert.Engine.SearchAPI.RootSearchConfig : Type

Configuration for root finding search

• maxDepth : ℕ

  Maximum bisection depth

• tolerance : ℚ

  Tolerance for interval width

• taylorDepth : ℕ

  Taylor depth for interval evaluation

def LeanCert.Engine.SearchAPI.instReprRootSearchConfig.repr : RootSearchConfig → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Engine.SearchAPI.instReprRootSearchConfig : Repr RootSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instReprRootSearchConfig = { reprPrec := LeanCert.Engine.SearchAPI.instReprRootSearchConfig.repr }

def LeanCert.Engine.SearchAPI.instInhabitedRootSearchConfig.default : RootSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instInhabitedRootSearchConfig.default = { maxDepth := default, tolerance := default, taylorDepth := default }

instance LeanCert.Engine.SearchAPI.instInhabitedRootSearchConfig : Inhabited RootSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instInhabitedRootSearchConfig = { default := LeanCert.Engine.SearchAPI.instInhabitedRootSearchConfig.default }

structure LeanCert.Engine.SearchAPI.RootExistenceProof (e : Core.Expr) (I : Core.IntervalRat) : Prop

Proof that a root exists in the given interval.

This structure bundles an interval with a proof that there exists a point x in the interval where f(x) = 0.

• supported : ExprSupportedCore e

  Proof that the expression is supported (for correctness theorems)

• continuous : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)

  Proof of continuity on the interval

• hasRoot : ∃ x ∈ I, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

  The actual root existence proof

structure LeanCert.Engine.SearchAPI.UniqueRootProof (e : Core.Expr) (I : Core.IntervalRat) extends LeanCert.Engine.SearchAPI.RootExistenceProof e I : Prop

Proof that a root exists AND is unique.

Extends RootExistenceProof with uniqueness: there is exactly one root.

• supported : ExprSupportedCore e
• continuous : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)
• hasRoot : ∃ x ∈ I, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0
• unique (x y : ℝ) : x ∈ I → y ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0 → Core.Expr.eval (fun (x : ℕ) => y) e = 0 → x = y

  Uniqueness: any two roots must be equal

structure LeanCert.Engine.SearchAPI.RootIsolation (e : Core.Expr) : Type

Result of root finding: an isolating interval with existence proof

• interval : Core.IntervalRat

  The isolating interval containing the root

• proof : RootExistenceProof e self.interval

  Proof that a root exists in this interval

noncomputable def LeanCert.Engine.SearchAPI.findRoots (e : Core.Expr) (hsupp : ExprSupportedCore e) (hdom : ∀ (J : Core.IntervalRat), Meta.exprContinuousDomainValid e (Set.Icc ↑J.lo ↑J.hi)) (I : Core.IntervalRat) (cfg : RootSearchConfig := { }) : List (RootIsolation e)

Find all roots of e in interval I, returning isolating intervals with existence proofs.

This wraps bisectRoot to find intervals with sign changes, then constructs existence proofs using the IVT (via verify_sign_change).

Equations

• One or more equations did not get rendered due to their size.

structure LeanCert.Engine.SearchAPI.UniqueRootResult (e : Core.Expr) (I : Core.IntervalRat) : Type

Result of unique root finding: an interval with existence and uniqueness proof. This is a Type, not a Prop, so it can be used in Option.

• supported : ExprSupportedCore e

  Proof that the expression is supported (for correctness theorems)

• continuous : ContinuousOn (fun (x : ℝ) => Core.Expr.eval (fun (x_1 : ℕ) => x) e) (Set.Icc ↑I.lo ↑I.hi)

  Proof of continuity on the interval

• hasRoot : ∃ x ∈ I, Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0

  The actual root existence proof

• unique (x y : ℝ) : x ∈ I → y ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e = 0 → Core.Expr.eval (fun (x : ℕ) => y) e = 0 → x = y

  Uniqueness: any two roots must be equal

noncomputable def LeanCert.Engine.SearchAPI.findUniqueRoot (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (cfg : RootSearchConfig := { }) : Option (UniqueRootResult e I)

Find a unique root with existence AND uniqueness proof.

This wraps Newton contraction checking to find intervals where:

1. A root exists (via contraction or sign change)
2. The root is unique (via derivative being bounded away from 0)

Requires UsesOnlyVar0 e for the Newton contraction proof to work. Returns none if no unique root can be verified.

Equations

• One or more equations did not get rendered due to their size.

Optimization API (0.1.2)

structure LeanCert.Engine.SearchAPI.OptSearchConfig : Type

Configuration for optimization search

• maxIterations : ℕ

  Maximum iterations for branch-and-bound

• tolerance : ℚ

  Tolerance for box width

• useMonotonicity : Bool

  Use monotonicity pruning

• taylorDepth : ℕ

  Taylor depth for interval evaluation

instance LeanCert.Engine.SearchAPI.instReprOptSearchConfig : Repr OptSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instReprOptSearchConfig = { reprPrec := LeanCert.Engine.SearchAPI.instReprOptSearchConfig.repr }

def LeanCert.Engine.SearchAPI.instReprOptSearchConfig.repr : OptSearchConfig → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.SearchAPI.instInhabitedOptSearchConfig.default : OptSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instInhabitedOptSearchConfig.default = { maxIterations := default, tolerance := default, useMonotonicity := default, taylorDepth := default }

instance LeanCert.Engine.SearchAPI.instInhabitedOptSearchConfig : Inhabited OptSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instInhabitedOptSearchConfig = { default := LeanCert.Engine.SearchAPI.instInhabitedOptSearchConfig.default }

structure LeanCert.Engine.SearchAPI.GlobalMinResult (e : Core.Expr) (B : Optimization.Box) : Type

Result of global minimization with proof.

Bundles the minimization result with proofs that:

1. minValue.lo is a valid lower bound for all x in B
2. There exists a point achieving a value ≤ minValue.hi

• minimizerBox : Optimization.Box

  Box containing the minimizer (best bound found here)

• minValue : Core.IntervalRat

  Interval containing the minimum value

• lowerBoundProof (ρ : ℕ → ℝ) : Optimization.Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ↑self.minValue.lo ≤ Core.Expr.eval ρ e

  Proof of the lower bound: ∀ x ∈ B, minValue.lo ≤ f(x)

• upperBoundWitness : ∃ (ρ : ℕ → ℝ), Optimization.Box.envMem ρ B ∧ (∀ i ≥ List.length B, ρ i = 0) ∧ Core.Expr.eval ρ e ≤ ↑self.minValue.hi

  Proof of the upper bound witness: ∃ x ∈ B, f(x) ≤ minValue.hi

structure LeanCert.Engine.SearchAPI.GlobalMaxResult (e : Core.Expr) (B : Optimization.Box) : Type

Result of global maximization with proof.

Bundles the maximization result with proofs that:

1. maxValue.hi is a valid upper bound for all x in B
2. There exists a point achieving a value ≥ maxValue.lo

• maximizerBox : Optimization.Box

  Box containing the maximizer (best bound found here)

• maxValue : Core.IntervalRat

  Interval containing the maximum value

• upperBoundProof (ρ : ℕ → ℝ) : Optimization.Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → Core.Expr.eval ρ e ≤ ↑self.maxValue.hi

  Proof of the upper bound: ∀ x ∈ B, f(x) ≤ maxValue.hi

• lowerBoundWitness : ∃ (ρ : ℕ → ℝ), Optimization.Box.envMem ρ B ∧ (∀ i ≥ List.length B, ρ i = 0) ∧ ↑self.maxValue.lo ≤ Core.Expr.eval ρ e

  Proof of the lower bound witness: ∃ x ∈ B, f(x) ≥ maxValue.lo

def LeanCert.Engine.SearchAPI.OptSearchConfig.toGlobalOptConfig (cfg : OptSearchConfig) : Optimization.GlobalOptConfig

Convert OptSearchConfig to GlobalOptConfig

Equations

• cfg.toGlobalOptConfig = { maxIterations := cfg.maxIterations, tolerance := cfg.tolerance, useMonotonicity := cfg.useMonotonicity, taylorDepth := cfg.taylorDepth }

noncomputable def LeanCert.Engine.SearchAPI.findGlobalMin (e : Core.Expr) (hsupp : ExprSupported e) (B : Optimization.Box) (cfg : OptSearchConfig := { }) : GlobalMinResult e B

Find global minimum of e over box B with proof.

This wraps globalMinimizeCore and bundles the result with correctness proofs derived from globalMinimizeCore_lo_correct.

Note: Uses ExprSupported (no log) for automatic domain validity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanCert.Engine.SearchAPI.findGlobalMax (e : Core.Expr) (hsupp : ExprSupported e) (B : Optimization.Box) (cfg : OptSearchConfig := { }) : GlobalMaxResult e B

Find global maximum of e over box B with proof.

This wraps globalMaximizeCore and bundles the result with correctness proofs.

Note: Uses ExprSupported (no log) for automatic domain validity.

Equations

• One or more equations did not get rendered due to their size.

1D Optimization Convenience APIs

structure LeanCert.Engine.SearchAPI.GlobalMin1DResult (e : Core.Expr) (I : Core.IntervalRat) : Type

Result of 1D global minimization with simplified proof structure

• minimizerInterval : Core.IntervalRat

  Interval containing the minimizer

• minValue : Core.IntervalRat

  Interval containing the minimum value

• lowerBoundProof (x : ℝ) : x ∈ I → ↑self.minValue.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

  Proof of the lower bound: ∀ x ∈ I, minValue.lo ≤ f(x)

structure LeanCert.Engine.SearchAPI.GlobalMax1DResult (e : Core.Expr) (I : Core.IntervalRat) : Type

Result of 1D global maximization with simplified proof structure

• maximizerInterval : Core.IntervalRat

  Interval containing the maximizer

• maxValue : Core.IntervalRat

  Interval containing the maximum value

• upperBoundProof (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑self.maxValue.hi

  Proof of the upper bound: ∀ x ∈ I, f(x) ≤ maxValue.hi

def LeanCert.Engine.SearchAPI.intervalToBox (I : Core.IntervalRat) : Optimization.Box

Convert IntervalRat to a 1D Box

Equations

• LeanCert.Engine.SearchAPI.intervalToBox I = [I]

noncomputable def LeanCert.Engine.SearchAPI.findGlobalMin1D (e : Core.Expr) (hsupp : ExprSupported e) (he1d : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (cfg : OptSearchConfig := { }) : GlobalMin1DResult e I

Find global minimum of e over 1D interval I with proof.

Specialized version for single-variable functions. Requires e.usesOnlyVar0 = true to ensure eval equivalence.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanCert.Engine.SearchAPI.findGlobalMax1D (e : Core.Expr) (hsupp : ExprSupported e) (he1d : e.usesOnlyVar0 = true) (I : Core.IntervalRat) (cfg : OptSearchConfig := { }) : GlobalMax1DResult e I

Find global maximum of e over 1D interval I with proof.

Specialized version for single-variable functions. Requires e.usesOnlyVar0 = true to ensure eval equivalence.

Equations

• One or more equations did not get rendered due to their size.

Integration API (0.1.3)

structure LeanCert.Engine.SearchAPI.IntegSearchConfig : Type

Configuration for integration search

• subdivisions : ℕ

  Number of subdivisions for uniform partitioning

• taylorDepth : ℕ

  Taylor depth for interval evaluation

def LeanCert.Engine.SearchAPI.instReprIntegSearchConfig.repr : IntegSearchConfig → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance LeanCert.Engine.SearchAPI.instReprIntegSearchConfig : Repr IntegSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instReprIntegSearchConfig = { reprPrec := LeanCert.Engine.SearchAPI.instReprIntegSearchConfig.repr }

instance LeanCert.Engine.SearchAPI.instInhabitedIntegSearchConfig : Inhabited IntegSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instInhabitedIntegSearchConfig = { default := LeanCert.Engine.SearchAPI.instInhabitedIntegSearchConfig.default }

def LeanCert.Engine.SearchAPI.instInhabitedIntegSearchConfig.default : IntegSearchConfig

Equations

• LeanCert.Engine.SearchAPI.instInhabitedIntegSearchConfig.default = { subdivisions := default, taylorDepth := default }

structure LeanCert.Engine.SearchAPI.IntegralResult (e : Core.Expr) (I : Core.IntervalRat) : Type

Result of verified integration.

Bundles the computed integral bounds with a proof that the true integral lies within those bounds.

• bounds : Core.IntervalRat

  Interval containing the true integral

• proof : ∫ (x : ℝ) in ↑I.lo..↑I.hi, Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ self.bounds

  Proof that the integral is in the bounds

noncomputable def LeanCert.Engine.SearchAPI.findIntegral (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (cfg : IntegSearchConfig := { }) (hdom : evalDomainValid1 e I { taylorDepth := cfg.taylorDepth }) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) : IntegralResult e I

Compute rigorous bounds on ∫[a,b] f(x) dx with proof.

This wraps integrateInterval1Core and bundles the result with the correctness proof from integrateInterval1Core_correct.

Equations

• LeanCert.Engine.SearchAPI.findIntegral e hsupp I cfg hdom hcontdom = { bounds := LeanCert.Validity.Integration.integrateInterval1Core e I { taylorDepth := cfg.taylorDepth }, proof := ⋯ }

noncomputable def LeanCert.Engine.SearchAPI.findIntegralWithTolerance (e : Core.Expr) (hsupp : ExprSupportedCore e) (I : Core.IntervalRat) (taylorDepth : ℕ := 10) (hdom : evalDomainValid1 e I { taylorDepth := taylorDepth }) (hcontdom : Meta.exprContinuousDomainValid e (Set.Icc ↑I.lo ↑I.hi)) (_tol : ℚ) (_htol : 0 < _tol) (_maxSubdiv : ℕ := 100) : IntegralResult e I

Compute integral bounds with specified accuracy target.

Automatically increases subdivision count until the bound width is below the target tolerance (or max subdivisions reached).

Equations

• One or more equations did not get rendered due to their size.

Convenience Functions for Common Cases

def LeanCert.Engine.SearchAPI.hasRootIn (e : Core.Expr) (I : Core.IntervalRat) (cfg : RootSearchConfig := { }) : Bool

Check if an expression has a root in an interval (boolean version)

Equations

• LeanCert.Engine.SearchAPI.hasRootIn e I cfg = LeanCert.Validity.RootFinding.checkSignChange e I { taylorDepth := cfg.taylorDepth }

def LeanCert.Engine.SearchAPI.isPositiveOn (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : Bool

Check if an expression is positive on an interval

Equations

• LeanCert.Engine.SearchAPI.isPositiveOn e I cfg = decide (0 < (LeanCert.Engine.evalIntervalCore1 e I cfg).lo)

def LeanCert.Engine.SearchAPI.isNegativeOn (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : Bool

Check if an expression is negative on an interval

Equations

• LeanCert.Engine.SearchAPI.isNegativeOn e I cfg = decide ((LeanCert.Engine.evalIntervalCore1 e I cfg).hi < 0)

def LeanCert.Engine.SearchAPI.getLowerBound (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : ℚ

Get a lower bound on the minimum value

Equations

• LeanCert.Engine.SearchAPI.getLowerBound e I cfg = (LeanCert.Engine.evalIntervalCore1 e I cfg).lo

def LeanCert.Engine.SearchAPI.getUpperBound (e : Core.Expr) (I : Core.IntervalRat) (cfg : EvalConfig := { }) : ℚ

Get an upper bound on the maximum value

Equations

• LeanCert.Engine.SearchAPI.getUpperBound e I cfg = (LeanCert.Engine.evalIntervalCore1 e I cfg).hi