Solver API

The Solver class is the main entry point for the Python SDK. It manages communication with the Lean kernel and handles the verification lifecycle.

Solver Class

leancert.solver.Solver

High-level interface for LeanCert verification.

Manages compilation and communication with the Lean kernel. Use as a context manager for automatic cleanup.

Example

with Solver() as solver: x = var('x') result = solver.find_bounds(x**2, {'x': (0, 1)})

__init__(client=None, auto_simplify=True)

Initialize the solver.

Parameters:

Name	Type	Description	Default
client	Optional[LeanClient]	Optional LeanClient instance. If None, creates a new one.	None
auto_simplify	bool	If True (default), automatically simplify expressions before sending to the kernel. This reduces the dependency problem in interval arithmetic by canceling like terms.	True

find_bounds(expr, domain, config=Config())

Find global minimum and maximum bounds.

Parameters:

Name	Type	Description	Default
expr	Expr	Expression to analyze.	required
domain	Union[Interval, Box, tuple, dict]	Domain specification (Interval, Box, tuple, or dict).	required
config	Config	Solver configuration. Use Config.dyadic() for high-performance evaluation on deep expressions, or Config.affine() for tighter bounds on expressions with repeated variables.	Config()

Returns:

Type	Description
BoundsResult	BoundsResult with verified min/max intervals.

Example

Standard rational backend

result = solver.find_bounds(x**2, {'x': (-1, 1)})

High-performance Dyadic backend (10-100x faster for deep exprs)

result = solver.find_bounds(deep_expr, domain, Config.dyadic())

Affine backend for tight bounds (solves dependency problem)

result = solver.find_bounds(x - x, {'x': (-1, 1)}, Config.affine())

find_roots(expr, domain, config=Config())

Find roots of a univariate expression.

Parameters:

Name	Type	Description	Default
expr	Expr	Expression to find roots of.	required
domain	Union[Interval, Box, tuple, dict]	Search domain.	required
config	Config	Solver configuration.	Config()

Returns:

Type	Description
RootsResult	RootsResult with root intervals.

find_unique_root(expr, domain, config=Config())

Find a unique root using Newton contraction.

This method uses Newton iteration to prove both existence AND uniqueness of a root. It's mathematically stronger than find_roots() which only proves existence via sign change.

Parameters:

Name	Type	Description	Default
expr	Expr	Expression to find root of.	required
domain	Union[Interval, Box, tuple, dict]	Search domain (1D interval).	required
config	Config	Solver configuration.	Config()

Returns:

Type	Description
UniqueRootResult	UniqueRootResult with unique=True if uniqueness proven.

verify_bound(expr, domain, upper=None, lower=None, config=Config(), method='adaptive')

Verify that expression satisfies given bounds with False Positive Filtering.

Pipeline: 1. Symbolic Simplification (handles dependency problem) 2. Global Optimization (Branch & Bound) 3. Counterexample Concretization (filters false positives)

Parameters:

Name	Type	Description	Default
expr	Expr	Expression to verify.	required
domain	Union[Interval, Box, tuple, dict]	Domain specification.	required
upper	Optional[float]	Upper bound to verify (expr <= upper).	None
lower	Optional[float]	Lower bound to verify (expr >= lower).	None
config	Config	Solver configuration.	Config()
method	str	Verification method - 'adaptive' (default, uses optimization with false positive filtering) or 'interval' (fast, conservative).	'adaptive'

Returns:

Type	Description
bool	True if verified.

Raises:

Type	Description
VerificationFailed	If bound verification fails AND is confirmed by concrete evaluation (not a false positive).
ValueError	If method is invalid or no bounds specified.

integrate(expr, domain, partitions=10, config=Config())

Compute rigorous integral bounds.

Parameters:

Name	Type	Description	Default
expr	Expr	Expression to integrate.	required
domain	Union[Interval, Box, tuple, dict]	Integration domain.	required
partitions	int	Number of partitions.	10
config	Config	Solver configuration.	Config()

Returns:

Type	Description
IntegralResult	IntegralResult with verified bounds.

Convenience Functions

These standalone functions use a default solver instance for quick scripting.

leancert.solver.find_bounds(expr, domain, config=Config())

Find global min/max bounds for an expression.

Source code in python/leancert/solver.py

def find_bounds(
    expr: Expr,
    domain: Union[Interval, Box, tuple, dict],
    config: Config = Config(),
) -> BoundsResult:
    """Find global min/max bounds for an expression."""
    return _get_solver().find_bounds(expr, domain, config)

leancert.solver.find_roots(expr, domain, config=Config())

Find roots of a univariate expression.

Source code in python/leancert/solver.py

def find_roots(
    expr: Expr,
    domain: Union[Interval, Box, tuple, dict],
    config: Config = Config(),
) -> RootsResult:
    """Find roots of a univariate expression."""
    return _get_solver().find_roots(expr, domain, config)

leancert.solver.find_unique_root(expr, domain, config=Config())

Find a unique root using Newton contraction.

This proves both existence AND uniqueness of a root.

Source code in python/leancert/solver.py

def find_unique_root(
    expr: Expr,
    domain: Union[Interval, Box, tuple, dict],
    config: Config = Config(),
) -> UniqueRootResult:
    """Find a unique root using Newton contraction.

    This proves both existence AND uniqueness of a root.
    """
    return _get_solver().find_unique_root(expr, domain, config)

leancert.solver.verify_bound(expr, domain, upper=None, lower=None, config=Config(), method='adaptive')

Verify that an expression satisfies bounds with false positive filtering.

This function uses global optimization with counterexample concretization to filter false positives caused by interval over-approximation.

Parameters:

Name	Type	Description	Default
expr	Expr	Expression to verify.	required
domain	Union[Interval, Box, tuple, dict]	Domain specification.	required
upper	Optional[float]	Upper bound to verify (expr <= upper).	None
lower	Optional[float]	Lower bound to verify (expr >= lower).	None
config	Config	Solver configuration.	Config()
method	str	'adaptive' (default, uses optimization with false positive filtering) or 'interval' (fast, conservative).	'adaptive'

Returns:

Type	Description
bool	True if verified.

Raises:

Type	Description
VerificationFailed	If bound verification fails AND is confirmed by concrete evaluation (not a false positive).

Source code in python/leancert/solver.py

def verify_bound(
    expr: Expr,
    domain: Union[Interval, Box, tuple, dict],
    upper: Optional[float] = None,
    lower: Optional[float] = None,
    config: Config = Config(),
    method: str = 'adaptive',
) -> bool:
    """Verify that an expression satisfies bounds with false positive filtering.

    This function uses global optimization with counterexample concretization
    to filter false positives caused by interval over-approximation.

    Args:
        expr: Expression to verify.
        domain: Domain specification.
        upper: Upper bound to verify (expr <= upper).
        lower: Lower bound to verify (expr >= lower).
        config: Solver configuration.
        method: 'adaptive' (default, uses optimization with false positive
               filtering) or 'interval' (fast, conservative).

    Returns:
        True if verified.

    Raises:
        VerificationFailed: If bound verification fails AND is confirmed by
                           concrete evaluation (not a false positive).
    """
    return _get_solver().verify_bound(expr, domain, upper, lower, config, method)

leancert.solver.integrate(expr, domain, partitions=10, config=Config())

Compute rigorous integral bounds.

Source code in python/leancert/solver.py

def integrate(
    expr: Expr,
    domain: Union[Interval, Box, tuple, dict],
    partitions: int = 10,
    config: Config = Config(),
) -> IntegralResult:
    """Compute rigorous integral bounds."""
    return _get_solver().integrate(expr, domain, partitions, config)