alkahest
Python API

Core API

The core API provides the expression pool, expression type, and result object.

ExprPool

class 
class ExprPool()
#source

An intern table that owns all expressions in a session.

Every symbol, integer, and composite expression is stored in an ExprPool. Expressions from different pools must not be mixed.

Methods
symbol(name, domain=None, commutative=None)
#source

Free symbol. domain defaults to the ambient alkahest.context(domain=...) and only then to Domain.Real.

The fallback exists because the domain is not decoration: it picks the SMT-LIB sort (Int vs Real) and hence the logic (QF_NIA vs QF_NRA), so a pool symbol built inside a domain=Domain.Integer block used to change the question being asked without changing any status a caller reads. Pass domain="real" explicitly to opt out.

pi()
#source

The constant π (parse("pi")). pool.symbol("pi") is an ordinary variable that merely prints as pi.

E()
#source

Euler's number e = exp(1) (parse("E")).

euler_gamma()
#source

The Euler–Mascheroni constant γ ≈ 0.5772 (parse("EulerGamma")).

catalan()
#source

Catalan's constant G ≈ 0.9160 (parse("Catalan")).

golden_ratio()
#source

The golden ratio φ = (1 + √5)/2 (parse("GoldenRatio")).

glaisher()
#source

The Glaisher–Kinkelin constant A ≈ 1.2824 (parse("Glaisher")).

imaginary_unit()
#source

Canonical imaginary unit I (Domain.Complex symbol named "I").

In evaluate(..., mode="complex") this auto-binds to 1j when unbound. Symbolic simplification folds I**2 → -1, etc.

integer(n)
#source

Intern an exact integer constant.

rational(p, q)
#source

Exact rational p/q. Both take Python ints of any size, as [integer] does — see big_integer_from_py.

func(name, args)
#source

Apply a named primitive or symbolic function: pool.func("sin", [x]), pool.func("f", [n]).

A built-in name at the wrong number of arguments (pool.func("sqrt", [])`, `pool.func("EllipticPi", [x])`) raises `PoolError (E-POOL-002); a name that is not built in takes any number.

add(args)
#source

Build an addition node: pool.add([x, y, z]) → x + y + z.

Children are sorted canonically so pool.add([b, a]) == pool.add([a, b]).

This is the bulk path for a large sum: one call interns one node, so it is linear in len(args). Accumulating with s = s + t (or the builtin sum()) interns a new, one-wider Add at every step — quadratic in time and in pool memory, which the pool never gives back.

Every argument must come from this pool; one from another pool raises PoolError (E-POOL-001).

mul(args)
#source

Build a multiplication node: pool.mul([x, y, z]) → x * y * z.

The bulk path for a large product, as add is for a sum. Every argument must come from this pool (PoolError, E-POOL-001).

float(value, prec=None)
#source
big_o(arg)
#source

O(arg) — Landau remainder bound (V2-15 series API).

pos_infinity()
#source

Canonical +∞ for limit(..., oo) (Unicode ∞, V2-16).

neg_infinity()
#source

Canonical -∞ (-1 · ∞), the same expression as -pool.pos_infinity().

lt(a, b)
#source
le(a, b)
#source
gt(a, b)
#source
ge(a, b)
#source
pred_eq(a, b)
#source
pred_ne(a, b)
#source
pred_and(args)
#source
pred_or(args)
#source
pred_not(a)
#source
pred_true()
#source
pred_false()
#source
forall(var, body)
#source

Universal quantifier: ∀ var . body (first-order logic).

exists(var, body)
#source

Existential quantifier: ∃ var . body.

save_to(path)
#source

Write the pool to path atomically (temp + rename). Raises IoError on any filesystem failure.

load_from(path)
staticmethod
#source

Load a persisted pool from path. Returns a new ExprPool. Raises FileNotFoundError if path does not exist, IoError for other failures.

Expr

class 
class Expr
#source

A handle to an interned expression node. Expr objects support Python arithmetic operators which build new expressions in the same pool.

+, -, *, **, / all produce new Expr objects:

Python
pool = ExprPool()
x = pool.symbol("x")
expr = x**2 + pool.integer(3) * x - pool.integer(1)

Symbol("x", "real") and Symbol("x", "complex") are distinct expressions with different ExprIds. Domains are part of structural identity, not a global assumption.

Methods
display_latex()
#source
display_unicode()
#source
pow_expr(exp)
#source
node_tag()
#source
node()
#source

DerivedResult

class 
class DerivedResult
#source

The return type of diff, simplify, integrate, and all top-level operations.

Example:

Python
dr = diff(sin(x**2), x)
print(dr.value)   # 2*x*cos(x^2)
for step in dr.steps:
    print(step['rule'], step['before'], "→", step['after'])
print(dr.to_dict(mode="compact")["verification"]["status"])
Properties
value
#source

The result expression (Expr).

derivation
#source
steps
#source

List of rewrite steps. Each step is a dict with keys:

  • rule (str) — rule name
  • before (str) — expression before the rewrite
  • after (str) — expression after the rewrite
  • side_conditions (list[str]) — conditions recorded for the rewrite
side_conditions
#source

Every side condition recorded by the derivation, flattened and de-duplicated (["x != 0", ...]).

For diff() / diff_forward() of abs, sign, floor, ceil, round, min or max these are the points where the almost-everywhere derivative returned does not hold (the kinks and jumps); empty for a smooth expression.

certificate
#source

Lean 4 proof certificate (.lean source), when the derivation log is certifiable without sorry and without false unwrapped equalities.

Returns None when the log is empty, records an integration (where integrand = F would be false), the Tendsto emitter does not recognise the limit pattern, or the proof would require an admission (B3).

certificate_status
#source

Why this result does (or does not) carry a Lean certificate.

Returns a dict with:

  • certifiable — True iff certificate is not None.
  • reason — stable reason code: "emitted", "withheld_no_derivation" (nothing was rewritten, so there is nothing to prove), "withheld_integration_shape" (the integral falls outside the FTC fragment the emitter can encode), "withheld_tendsto_shape" (the limit falls outside the Filter.Tendsto fragment the emitter can encode), "withheld_gosper_shape" (the sum falls outside the Finset telescope fragment), "withheld_product_shape" (the product is not the ∏ k = n! identity), "withheld_resultant_shape" (the Sylvester matrix is larger than 7×7 or a coefficient is too large), or "withheld_uncertifiable_step".
  • blocking_steps — for withheld_uncertifiable_step, the list of {"index", "rule", "before", "after"} records whose rewrite rule has no sound Lean encoding today. This is a diagnostic: an empty list with certifiable=False means the whole-derivation gate withheld for a reason not attributable to a single step.

The certifiability boundary this reports is exactly the one tabulated by certificate_coverage().

verification
#source

Machine-readable evidence metadata for this derived result.

A generated Lean source artifact is not a statement that Lean has checked it. An indefinite integration result is exactly_verified only when its symbolic derivative residual simplifies to zero.

Methods
to_dict(mode="full")
#source

Stable, versioned dict envelope for machine/agent consumers.

mode="full" (default) carries the same information as .steps / .verification / .certificate_status combined under one discriminated envelope (kind="alkahest.derived_result", versioned by SCHEMA_VERSION / STEPS_SCHEMA_VERSION).

mode="compact" is strictly smaller and intended for hot loops / tight agent context budgets:

  • steps entries drop before/after (usually the largest strings in a derivation — the single biggest token cost) and use short keys: r (rule name) and s (side_conditions, omitted entirely when the list is empty).
  • verification is pruned to status and externally_verified only — the two fields that carry the honesty signal (whether this result is verified, and whether that verification happened out-of-process). verification["status"] is never renamed, abbreviated, or omitted in compact mode.
  • certificate_status is pruned to certifiable and reason; the blocking_steps diagnostic list (which repeats before/after expression text) is dropped.

Neither mode ever includes the Lean certificate source text — use the certificate getter for that. has_certificate (a bool) plus certificate_status.reason is enough to know whether a certificate exists and why not, without paying for the source.

Raises ValueError for any mode other than "full" / "compact".

to_json(mode="full")
#source

json.dumps(self.to_dict(mode=mode)), via Python's own json module so the output matches what an agent's own json.dumps would produce. See to_dict() for the schema.

Context manager

function 
context(
    *,
    pool: Any=None,
    domain: Any=None,
    simplify: bool=False,
    precision: int | None=None,
    assumptions: Any=None,
    require_certificate: bool | None=None,
    budget: Budget | None=None,
    **extra: Any
) → Generator[None, None, None]
#source

Thread-local context for Alkahest calls.

Parameters
poolExprPool, optional

Default expression pool used by alkahest.symbol and other pool-aware helpers when called without an explicit pool argument.

domainstr or Domain, optional

Default domain for symbol construction that omits domain — both alkahest.symbol(name) and pool.symbol(name) (e.g. "real", Domain.Integer). The two agree deliberately: the domain picks the SMT-LIB sort (Int vs Real), so a constructor that ignored it would change the question alkahest.smt.solve answers without changing any status a caller reads. Pass an explicit domain= to either constructor to override the block.

simplifybool

When True, diff(), integrate(), sum_indefinite(), sum_definite(), product_indefinite(), and product_definite() post-process their DerivedResult with simplify() (see simplify_enabled()). Explicit simplify() / simplify_trig() calls are unchanged.

precisionint, optional

Default MPFR precision in bits for ball-arithmetic operations.

assumptionsAssumptions, optional

Default Assumptions context, scoped to pool. simplify(), simplify_log_exp(), and solve() pick this up automatically when called without an explicit assumptions/domain argument of their own (see active_assumptions()). Explicit arguments to those functions always take precedence over the context.

The block additionally installs the facts on the Rust side for the engines that consult them indirectly. limit() reads stated signs of free parameters, and integrate() reaches it for any bound of ±∞, so ∫₀^∞ e^{-ke·t} dt returns 1/ke under ke > 0 and refuses with E-LIMIT-006 — naming ke — when nothing is stated. A symbol declared Domain.Positive carries the same fact without a context.

require_certificatebool, optional

When True, every derivation-producing call in the block (diff(), integrate(), the simplify() family, the sum/product solvers) must yield a Lean certificate, or it raises CertificateUnavailableError (E-CERT-001) instead of returning an uncertified result. This is the ambient form of require_certificate(); use it to stop a research loop from silently accumulating claims it cannot back up. Pass False in an inner block to opt back out.

budgetBudget, optional

P1 search plumbing item 4. When set, pushes a wall-clock / step budget and a determinism seed into the Rust-side cooperative checkpoint (alkahest_core::budget) for the scope of this block. integrate() raises BudgetExceededError (E-BUDGET-*) if the budget trips; request_cancel() trips it from another thread. Like every other context key, a nested context(budget=...) shadows this one rather than merging with it — see Budget and docs/mdbook/src/budgets.md.

**extra

Additional key-value pairs stored in the context and accessible via get_context_value().

Notes

Contexts are thread-local and nest — inner contexts shadow outer ones for any keys they define. The kernel remains fully stateless; this module is an ergonomic Python wrapper only.

Examples
Python
>>> import alkahest
>>> p = alkahest.ExprPool()
>>> with alkahest.context(pool=p, domain="real"):
...     x = alkahest.symbol("x")
...     y = alkahest.symbol("y")
...     expr = x ** 2 + y ** 2

Contexts nest (inner keys shadow outer ones):

Python
with alkahest.context(pool=p):
    with alkahest.context(domain="integer"):
        # pool from outer context; domain overridden here.
        ...

Assumptions flow through to assumption-aware simplifiers:

Python
>>> x = p.symbol("x")
>>> assumptions = alkahest.Assumptions(p)
>>> assumptions.refine(p.gt(x, p.integer(0)))
>>> with alkahest.context(pool=p, assumptions=assumptions):
...     alkahest.simplify_log_exp(alkahest.exp(alkahest.log(x))).value  # x
function 
symbol(
    name: str,
    *,
    pool: Any=None,
    domain: Any=None,
    commutative: bool=True
) → Any
#source

Create a symbol, inferring pool and domain from the active context.

pool.symbol(name) infers the domain from the same context, so the two constructors agree; this one additionally infers the pool.

Parameters
namestr

Symbol name.

poolExprPool, optional

Explicit pool; overrides the context pool.

domainstr or Domain, optional

Explicit domain; overrides the context domain.

commutativebool

When False, the symbol does not commute under multiplication (V3-2).

Returns
Expr

The interned symbol expression.

Notes

With no pool and no alkahest.context(pool=...) block open, the symbol is created in default_pool() — the same pool alkahest.parse(text) and alkahest.sin(2) use — so x = alkahest.symbol("x") works on its own.

function 
active_pool() → Any | None
#source

Return the pool from the innermost active context, or None.

function 
simplify_enabled() → bool
#source

Return True if the active context has simplify=True.

Parsing

function 
parse(
    source: str,
    pool=None,
    symbols: dict[str, object] | None=None
)
#source

Parse a mathematical expression string into an Expr.

Uses a Pratt (top-down operator precedence) recursive-descent parser.

Parameters
sourcestr

Expression string, e.g. "sin(x)^2 + cos(x)^2".

poolExprPool, optional

Expression pool used to intern new symbols and constants. Defaults to the pool of the active alkahest.context(pool=...) block, else default_pool().

symbolsdict[str, Expr] | None

Optional pre-bound symbol map. Identifiers not in the map are created via pool.symbol(name) and added to the map so they are reused within the same call.

Reserved names, read as constants when not in the map (so that parse(str(e)) == e): I is ExprPool.imaginary_unit(), E is exp(1), oo and ∞ are ExprPool.pos_infinity(); pi, EulerGamma, Catalan, Glaisher and GoldenRatio are the constants ExprPool.pi(), ExprPool.euler_gamma(), … that every evaluator knows the value of. To use one of these names as a variable, bind it: parse("E*x", pool, {"E": pool.symbol("E")}) (pool.symbol("pi") is such a variable — it prints as pi but is not π). 3/4 between integer literals is the exact rational 3/4.

Returns
Expr

The parsed expression.

Raises
ParseError

On a lexical or syntax error, with .span set to the byte range of the offending token.

Examples
Python
>>> import alkahest
>>> pool = alkahest.ExprPool()
>>> x = pool.symbol("x")
>>> e = alkahest.parse("x^2 + 2*x + 1", pool, {"x": x})
>>> alkahest.parse("sin(x)^2 + cos(x)^2", pool, {"x": x})
sin(x)^2 + cos(x)^2

Assumptions and context

class 
class Assumptions(pool)
#source

Pool-scoped assumptions for conservative simplification (stable top-level).

Properties
predicates
#source

Predicates explicitly asserted in this context.

Methods
refine(predicate)
#source

Add a predicate to this context.

Only positive and non-zero facts authorize conditional rewrites. Other predicates remain provenance for contradiction detection.

simplify(expr)
#source

Simplify an expression under this explicit assumption context.

Takes slf rather than &self so the borrow of this object is released before the GIL is: the core call runs on a copy of the context (a couple of small vectors), and a refine on another thread meanwhile neither waits on this call nor meets a held borrow.

is_positive(expr)
#source

True when this context has a strict-positivity fact for expr — either an explicit refine(x > 0) or expr itself being declared with Domain.Positive.

Agent-facing helper for composing assumptions with other APIs (e.g. filtering solve roots) without exposing the internal SideCondition representation.

class 
class Domain
#source

Python-visible symbol domain (matches alkahest_core::kernel::Domain).

function 
active_assumptions() → Any | None
#source

Return the Assumptions from the innermost active context, or None if no context set one.

Used by simplify(), simplify_log_exp(), and solve() to fall back to a caller-established assumption context when they're invoked without their own assumptions argument.

function 
active_domain() → Any | None
#source

Return the domain from the innermost active context, or None.

function 
get_context_value(key: str, default: Any=None) → Any
#source

Return the value of key from the innermost active context, or default.

Version and capabilities

function 
version()
#source

Returns the alkahest-core version string.

constant 
__version__
#source
__version__ = _meta_version('alkahest')

No docstring.

function 
capabilities() → dict
#source

Return the versioned agent contract for this installed build.

Agents should call this once at session start before selecting an operation. The features mapping is authoritative for the installed extension; it does not infer availability from project defaults or Python fallback functions.

Note verification["oracles"] and verification["smt_solvers"] probe the environment: detecting an oracle imports it, and detecting a solver runs its binary to read a version. Both are cached for the life of the process, so the cost lands on the first call and not on later ones — but the first call is not free, and it is not a pure read of build metadata like the rest of this contract.

Because they are cached, these two keys are a session-start snapshot. A tool installed later in the same process will not appear here. smt.solvers() and crosscheck.oracles() re-probe on every call and are the live view.

Returns
dict

contract_version identifies this schema. groebner, jit, egraph, and parallel are compatibility feature booleans. features contains installed Cargo features and explicit llvm_jit / cranelift_jit backend flags — every key names something a caller can actually reach, which is why v3 drops groebner_cuda and numpy (see below); primitives is deterministic per-primitive implementation coverage, and verification describes available evidence artifacts and checkers. verification["coverage"] summarises the generated certificate ledger (certificate_coverage()), which is also where each primitive's lean_theorem bit comes from — so the capability bits and the coverage table cannot disagree.

Each primitives row also carries taylor_model: whether the validated-bounds subsystem (bound_on_box(), verified_integral(), verified_no_roots(), verified_sign()) has a rigorous Taylor-model rule for it, i.e. whether those entry points can bound it at all. It is a different question from numeric_ball, which is pointwise ball arithmetic: it is True for floor and ceil, neither of which can be bounded over a box, and it was True for erf, bessel_j0, digamma and six more before 3.9.0 gave them Taylor-model rules. Reading the latter as coverage is what made the boundary invisible. The bit is derived by running the Taylor evaluator, so it cannot drift from what bound_on_box accepts; bounds_supported() asks the same question for a whole expression.

Symbolic linear algebra (Matrix.rref, rank, nullspace, jordan_form, minimal_polynomial, LU/QR/Cholesky, etc.) is available on Matrix; unsupported inputs raise LinearAlgebraError with stable E-LINALG-* codes.

Notes

Contract v3 removed two features keys. Code that indexes caps["features"]["groebner_cuda"] or ["numpy"] now raises KeyError; use .get(name, False) if you must span versions, and gate on contract_version when the distinction matters.

Both were removed rather than wired up because neither was falsifiable. groebner_cuda reported that the GPU Gröbner kernel was compiled in, but that kernel has no Python binding at all — GroebnerBasis.compute, solve() and triangularize() run on the CPU whatever it said, so no observation a caller could make distinguished True from False. numpy reported a Cargo feature gating a crate the extension never used; numpy_eval() goes through the buffer protocol and works identically with the bit False, which is its value on every build ever shipped. A bit that reads False honestly is better than one that reads True and lies, and a bit that correlates with nothing is better removed than left to be misread.

features also carries two bits that are not Cargo features: arb_backend and riemann_theta. alkahest-core/build.rs probes libflint's symbol table for them, because FLINT absorbed Arb in 3.0 but rewrote the acb_theta API in 3.2 — so the same Cargo invocation against an older FLINT produces a build whose theta module is entirely stubbed. Both bits satisfy the falsifiability rule above: False guarantees every entry point behind them raises E-THETA-001 instead of computing, so the two states are distinguishable by observation rather than by trust. Check caps["features"]["riemann_theta"] before calling riemann_theta(). contract_version stays 3: the row gained keys and lost none.

Examples
Python
>>> import alkahest as ak
>>> caps = ak.capabilities()
>>> if caps["groebner"]:
...     result = ak.solve([x**2 - 1], [x])
>>> if not caps["jit"]:
...     print("JIT unavailable; compile_expr will run in interpreter mode")
constant 
HAS_EGRAPH
#

No docstring.

function 
jit_is_available()
#source

Return True if any native JIT backend is available in this build.

When False, compile_expr falls back to the tree-walking interpreter and emits a RuntimeWarning.