exprtest

exprtest provides fast predicates for mathematical expressions (including exact numeric ones). Its currently primary API, zerotest(), returns True only for a proved zero. By default it returns False for either a proved nonzero value or strong one-sided evidence of nonzeroness, and None when neither conclusion is available. Use confidence="certified" when False must mean proved nonzero.

The package combines specialized SymPy-based exact methods with rigorous Arb/Acb ball arithmetic from python-flint. Numerical guesses and probabilistic evidence never become a proof without an independent certificate. The default probable policy may use strong one-sided nonzero evidence for a False result; users can request certified-only Boolean semantics explicitly.

Installation

pip install exprtest

Install the rigorous Arb/FLINT backend when you want ball-arithmetic and FLINT-accelerated proofs:

pip install "exprtest[flint]"

For development with the full backend:

pip install -e ".[dev]"
pytest

Quick start

import sympy as sp
from exprtest import is_algebraic, is_prime, zerotest

x = sp.symbols("x")

assert zerotest(0) is True
assert zerotest(sp.pi) is False
assert zerotest(sp.Function("f")(x)) is None

assert is_prime(97) is True
assert is_algebraic(sp.sqrt(2)) is True
assert is_algebraic(sp.pi) is False

For a complete executable example, see examples/quickstart.py.

Proof semantics

zerotest(expr) defaults to probable semantics: strong one-sided NONZERO_LIKELY evidence may map to False; probabilistic zero-like evidence is never promoted to True. Use zerotest(expr, confidence="certified") when both Boolean outcomes must be certified. Use profile_zerotest() when you need the method, evidence, or stage timings.

from exprtest import profile_zerotest

profile = profile_zerotest(sp.exp(sp.sqrt(2), evaluate=False))
assert profile.result is False
print(profile.classification.method)
print(profile.classification.evidence)

The distinction between exact proof, rigorous enclosure, probabilistic evidence, and heuristic candidate generation is described in docs/soundness.md.

What the fast oracle handles

The normal oracle uses bounded, structure-specific methods rather than general symbolic simplification. Important classes include exact rational arithmetic, small algebraic towers and radicals, bounded polynomial/rational identities, assumption-aware nonzero and definedness proofs, roots of unity and exact trigonometric/power identities, branch-safe logarithmic/exponential relations, selected exact special-function values, bounded exponential-independence theorems, rigorous Arb/Acb enclosures, and finite-field testing for suitable rational functions.

Potentially expensive stages are admitted by structural budgets. Sparse tower arithmetic, cached expression fingerprints, per-call fact memoization, and adaptive precision selection keep common cases inexpensive.

Function-property knowledge

exprtest includes a small registry of SymPy-native function facts, including selected real/sign properties, complex-domain restrictions, and simple pole sets. The active entries are regression-tested against the documented SymPy semantics used by the package. This improves zerotest() as well as public predicates such as is_real() and is_integer() without adding a runtime dependency. The registry is documented in docs/function_facts.md.

A capability overview is available in docs/capabilities.md.

Number predicates

The package exposes tri-state predicates for common number domains:

from exprtest import (
    ElementOf,
    is_algebraic,
    is_integer,
    is_prime,
    is_rational,
    is_real,
    number_kind,
)

Each predicate returns True, False, or None according to what the bounded proof engine can establish. ElementOf() performs lightweight membership simplification, and number_kind() distinguishes values proved algebraic, proved transcendental, or unresolved.

See docs/api.md for the supported public interface.

Performance model

zerotest() is intended to be a fast heuristic, so does not call general sympy.simplify(), trigsimp(), or together() on its latency-sensitive path. Expensive algebraic operations are size-gated and time-bounded. Stronger separation bounds and higher Arb precision are requested only when cheaper certificates are insufficient.

benchmarks/benchmark_zerotest.py measures cold and repeated-call throughput, median latency, p95 latency, and verdict counts. Benchmark numbers are machine specific; routing and proof-stage assertions in the test suite enforce the performance architecture independently of wall-clock timing. CI also records branch coverage and runs a separate structural performance-contract job.

More detail is in docs/performance.md.

Limitations

exprtest is intentionally incomplete. General symbolic identities with free variables, high-degree algebraic extensions, difficult branch-sensitive complex identities, and transcendental combinations outside known theorems may return None. Algebraic independence questions that are unknown in mathematics remain unknown to the package. And, of course, zero testing in general is undecidable.

See docs/limitations.md for the main boundaries and planned extensions.

Documentation

• API
• Architecture
• Capabilities
• Soundness
• Performance
• Assumptions and branches
• Limitations
• Development

License

exprtest is free software licensed under the GNU General Public License v3.0 (GPL-3.0-only). See LICENSE for the full license text.