Alkahest

A high-performance computer algebra system for Python built for both humans and agents. Symbolic operations run orders of magnitude faster than SymPy and can run on modern accelerated hardware. Every computation produces a derivation log; a meaningful subset can export Lean 4 proofs for independent verification.

Install: the package is published on PyPI; use pip install alkahest (Python 3.9–3.13). Default wheels ship Cranelift CPU JIT (pure Rust, no LLVM). See Install for the capability matrix and optional +jit / +full Linux wheels (GitHub Releases).

Demo: try the hosted playground (WASM in-browser, or bring your own server/Jupyter URL + token), or run demo-playground/ locally for the full agent and recording stack. See demo-playground/README.md.

Links: GitHub · RL environment (alkahest/alkahest-symbolic-integration on Prime Intellect Environments Hub)

Stack: Rust kernel → FLINT/Arb (polynomials, ball arithmetic) → vendored egglog + colored e-graphs (simplification) → Cranelift/LLVM JIT + MLIR (native and GPU codegen) → PyO3 → Python

Install

Requirements: Python 3.9–3.13 (PyPI requires-python).

pip install alkahest

RL environments (symbolic integration tasks for Prime Intellect / veRL): Python ≥ 3.10 required.

pip install "alkahest[rl]"

See Reinforcement learning and the RL guide.

For an isolated environment (recommended when juggling versions or building from source):

python3 -m venv .venv && source .venv/bin/activate   # Windows: .venv\Scripts\activate
python -m pip install -U pip
pip install alkahest

Default PyPI wheels include the vendored egglog e-graph backend (egraph), the Gröbner solver (groebner — so alkahest.solve, Diophantine, homotopy, and related APIs work out of the box), and Cranelift Tier-1 CPU JIT (cranelift, pure Rust, ~2 MB larger than the interpreter-only baseline). They do not include LLVM JIT or parallel. For LLVM CPU JIT—or JIT plus parallel F4—use a PyTorch-style opt-in +jit / +full Linux wheel from GitHub Releases, not the default PyPI resolver path.

Install matrix (default vs opt-in wheels)

Probe your environment after install: alkahest.capabilities()["features"] and alkahest.jit_is_available().

macOS / Windows: default PyPI wheels include Cranelift JIT. +jit and +full are not built in CI (LLVM / MSYS2 constraints); use building from source with --features jit (and parallel for F4 parallelism) on those platforms.

Linux LLVM wheels vendor LLVM and related .so files under site-packages/alkahest.libs/. If import alkahest fails with a missing libffi-*.so or libLLVM-*.so, prepend that directory to LD_LIBRARY_PATH.

Opt-in Linux wheels: +jit and +full (PyTorch-style)

Why a separate index or direct wheel URL: feature-heavy wheels use a PEP 440 local version (for example 2.0.3+jit or 2.0.3+full). Those builds must not be mixed into the main PyPI project’s simple API for the same reason PyTorch publishes CUDA wheels on download.pytorch.org: otherwise pip install alkahest could resolve a +jit / +full build as “newer” than 2.0.3 and pull LLVM (or a much larger binary) when you wanted the default wheel.

There is no pip install alkahest[jit] / alkahest[full] that swaps the native extension: pip extras only add Python dependencies, not alternate binaries for the same wheel slot.

Until a dedicated PEP 503 simple index is published, tagged releases attach Linux linux_x86_64 wheels on GitHub Releases (CI builds them on ubuntu-22.04, not the manylinux image used for default wheels). Pick the .whl whose tags match your Python (cp311, etc.) and linux_x86_64.

Direct-install examples (adjust tag and filename after checking the release assets):

pip install "https://github.com/alkahest-cas/alkahest/releases/download/v2.3.1/alkahest-2.3.1+full-cp311-cp311-linux_x86_64.whl"
pip install "https://github.com/alkahest-cas/alkahest/releases/download/v2.3.1/alkahest-2.3.1+jit-cp311-cp311-linux_x86_64.whl"

These wheels vendor LLVM (for JIT) and related .so files under site-packages/alkahest.libs/. If import alkahest fails with a missing libffi-*.so or libLLVM-*.so, prepend that directory to LD_LIBRARY_PATH (or install matching system packages). Release CI uses the same LD_LIBRARY_PATH step when smoke-testing wheels.

If your client chokes on + in the URL, use percent-encoding (2.3.1%2Bfull in the filename segment).

After installing the default wheel, alkahest.jit_is_available() is True (Cranelift). After +jit or +full, it is also True (LLVM). Gröbner-backed APIs such as alkahest.solve are available in all wheels since groebner became a default feature.

See the install matrix for per-platform coverage.

Target layout (roadmap): a small extra index URL (PEP 503) hosting only +jit / +full wheels, mirroring PyTorch’s --extra-index-url workflow:

pip install 'alkahest==2.0.3+full' --extra-index-url https://EXAMPLE/alkahest-extras/simple

From source

Required to enable optional features (jit, cuda, parallel) or for development. The groebner and egraph features are already built into default wheels; a source build inherits them automatically. Prerequisites:

• Rust stable ≥ 1.76 and nightly:

  curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
  rustup toolchain install nightly
  

• uv (recommended Python tool manager): curl -LsSf https://astral.sh/uv/install.sh | sh
• LLVM 15: apt install llvm-15 libllvm15 llvm-15-dev / brew install llvm@15
• FLINT ≥ 2.9 (includes GMP and MPFR): apt install libflint-dev / brew install flint

# Install dev tools (maturin, pytest, ruff, ty, …) without building the Rust extension:
uv sync --no-install-project --group dev
# Build and install the extension into the project venv:
uv run maturin develop --manifest-path alkahest-py/Cargo.toml --release --features "parallel egraph jit groebner"

Without uv, install maturin directly and run the same develop command:

pip install maturin
maturin develop --manifest-path alkahest-py/Cargo.toml --release --features "parallel egraph jit groebner"

Optional Cargo features: parallel (sharded pool + parallel F4 + numpy_eval_par), egraph (vendored egglog backend; default in PyPI wheels), groebner (Gröbner solver + Diophantine + homotopy; default in both the Rust crate and PyPI wheels), cranelift (pure-Rust Tier-1 JIT), jit (LLVM JIT), cuda (NVPTX codegen).

Rust crate

alkahest-cas is also published on crates.io (docs.rs) for use directly from Rust without a Python runtime:

[dependencies]
alkahest-cas = "2"

# groebner is included by default; add other optional features as needed:
# alkahest-cas = { version = "2", features = ["parallel", "egraph"] }

System prerequisites (same libraries as the Python build — must be present before cargo build):

# Debian / Ubuntu
sudo apt-get install -y libflint-dev libgmp-dev libmpfr-dev

# macOS
brew install flint

The jit feature additionally requires LLVM 15 dev headers (apt install llvm-15-dev / brew install llvm@15). A self-contained runnable example is in examples/rust_quickstart/.

Quick start

import alkahest as ak

caps = ak.capabilities()  # groebner, jit, egraph, parallel
pool = ak.ExprPool()
x = pool.symbol("x")

# Python int literals work in arithmetic (pool still required for symbols)
expr = x**2 + 1

# Differentiation with derivation log
result = ak.diff(ak.sin(expr), x)
print(result.value)   # 2*x*cos(x^2)
print(result.steps)   # list of rewrite steps

# Integration
r = ak.integrate(ak.exp(x), x)
print(r.value)        # exp(x)

# Simplification — use simplify_trig for sin²+cos², not the catch-all simplify
s = ak.simplify(x + 0)
print(s.value)        # x
print(ak.simplify_trig(ak.sin(x)**2 + ak.cos(x)**2).value)  # 1

# JIT-compile to native code (interpreter fallback when caps["jit"] is False)
f = ak.compile_expr(x**2 + 1, [x])
print(f([3.0]))       # 10.0

Partial fractions, definite integration, and Lean certificates:

import alkahest as ak

pool = ak.ExprPool()
x = pool.symbol("x")

f = 1 / (x**2 - pool.integer(1))
print(ak.apart(f, x))  # partial fractions over ℚ

r = ak.integrate(x**2, x, pool.integer(0), pool.integer(1))  # ∫₀¹ x² dx = 1/3
print(r.value)
print(r.certificate)  # Lean 4 proof term when available

More runnable examples live in examples/ — polynomials, Risch integration, Lean certificates, agent workflows, and more.

Expression representations

Representation types are explicit — no silent performance cliffs. Conversion between them is always an opt-in call (UniPoly.from_symbolic(...), etc.).

Result objects

Every top-level operation returns a DerivedResult with:

• .value — the result expression
• .steps — derivation log (list of rewrite rules applied)
• .certificate — Lean 4 proof term, when available

Reinforcement learning

alkahest.rl exposes verifiable RL environments backed by the CAS. The core layer (alkahest.rl.core) is trainer-agnostic; domain environments live under alkahest.rl.envs.* and optionally integrate with Prime Intellect Verifiers.

pip install "alkahest[rl]"   # Python ≥ 3.10; adds verifiers + datasets

from alkahest.rl.envs.integration import IntegrationVerifier, load_environment

verifier = IntegrationVerifier()
# reward = verifier.verify(model_output, {"f_expr": f, "is_elementary": True, "pool": pool})

env = load_environment(difficulty_tier=0, n_train=1000, n_eval=100, adaptive=True)

Environments Hub: alkahest/alkahest-symbolic-integration — install with prime env install alkahest/alkahest-symbolic-integration. Publish updates from python/alkahest/rl/envs/integration/ with prime env push. Full checklist in the RL guide.

Documentation and further reading

• Documentation site — full API reference and user guide
• ARCHITECTURE.md — crates, directory layout, and key files
• ROADMAP.md — planned milestones
• CONTRIBUTING.md — Rust vs Python layer guide
• TESTING.md — property-based testing, fuzzing, sanitizers, CI tiers
• BENCHMARKS.md — criterion and Python benchmark suites
• examples/ — runnable end-to-end examples
• LICENSE — Apache 2.0 license

Stability

Alkahest follows semantic versioning from 1.0. The stable surface is everything re-exported from alkahest_cas::stable (Rust) and alkahest.__all__ (Python). Experimental APIs live under alkahest_cas::experimental and alkahest.experimental and may change in minor releases.