alkahest documentation
alkahest is a computer algebra system with a Rust core and a Python API, built for both humans and agents. Every computation produces a derivation log, a growing subset exports Lean 4 proofs, and when it cannot answer it refuses with a coded error.
The API is still moving and alkahest will contain bugs, including answers that are wrong without saying so. Treat a result that matters as unverified until you have checked it: read the derivation log, export the Lean certificate where one exists, or cross-check against an independent source.
Install
pip install alkahestPython 3.10 to 3.14. The default wheel includes the e-graph simplifier, the Gröbner solver, the Cranelift JIT and the multi-core paths. LLVM JIT builds are on GitHub Releases; see Getting started.
cargo add alkahest-casThe crate is alkahest-cas. It needs FLINT 3.3 or newer, GMP and MPFR at build time (apt install libflint-dev libgmp-dev libmpfr-dev, brew install flint). API docs are on docs.rs.
Quickstart
Every computation starts with an ExprPool, which owns the expressions. Operations return a DerivedResult whose .value is the answer and whose .steps record how it was reached.
import alkahest as ak
from alkahest import ExprPool, cos, diff, exp, integrate, simplify_trig, sin
pool = ExprPool()
x = pool.symbol("x")
# Differentiate. Every result carries a derivation log in .steps
d = diff(sin(x**2), x)
print(d.value) # (x * 2 * cos(x^2))
# Integrate, and ask how the answer was checked
r = integrate(x * exp(x), x)
print(r.value) # (exp(x) * (x + -1))
print(r.verification["status"]) # exactly_verified
# Simplify a trigonometric identity
print(simplify_trig(sin(x) ** 2 + cos(x) ** 2).value) # 1
# Parse from a string, then take a limit
e = ak.parse("sin(x)/x", pool, {"x": x})
print(ak.limit(e, x, pool.integer(0)).value) # 1
# When there is no closed form, it refuses with a stable error code
try:
integrate(exp(x**2), x)
except ak.IntegrationError as err:
print(err.code) # E-INT-004: proven non-elementaryimport alkahest as ak
pool = ak.ExprPool()
x, y = pool.symbol("x"), pool.symbol("y")
# Exact solutions of a polynomial system (Gröbner bases)
print(ak.solve([x**2 + y**2 - 1, x - y], [x, y]))
# [{x: (sqrt(2) * (1/2)), y: (sqrt(2) * (1/2))},
# {x: (-1/2 * sqrt(2)), y: (-1/2 * sqrt(2))}]import alkahest as ak
pool = ak.ExprPool()
x = pool.symbol("x")
f = ak.sin(x) * ak.exp(x)
# JIT-compile to native code (Cranelift in the default wheel)
fast = ak.compile_expr(f, [x])
print(fast([0.5])) # 0.7904390832136149
# Or emit dependency-free C99
print(ak.emit_c_expr(f, [x], fn_name="f"))
# double f(double x) {
# return (exp(x) * sin(x));
# }import alkahest as ak
pool = ak.ExprPool()
x = pool.symbol("x")
# Bound the work a call may do; a trip raises BudgetExceededError
with ak.context(budget=ak.Budget(wall_ms=1000, max_steps=100_000)):
r = ak.diff(ak.sin(x) * ak.cos(x), x)
print(r.value) # (cos(x)^2 + (-1 * sin(x)^2))
# Export the derivation as Lean 4 source
print(ak.to_lean(r).splitlines()[0]) # import Mathlib.Tactic