AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities

Source: arXiv:2606.26442 · Published 2026-06-24 · By Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, Jannis Limperg

TL;DR

AXLE (Axiom Lean Engine) is a cloud infrastructure designed to support high-throughput, strict, and robust theorem proving utilities for the Lean 4 proof assistant. Motivated by recent AI advances in formal mathematics—such as reinforcement learning driven proof search and agentic proving workflows—AXLE addresses important limitations of existing Lean 4 tooling. These limitations include lack of scalable verification beyond compilation, single-version support, insufficient per-request isolation, and limited high-level proof manipulation capabilities. AXLE delivers a multi-tenant cloud service running 14 Lean metaprogramming tools for strict proof verification, semantic source-level transformations, lemma extraction, proof simplification and repair, and declaration metadata extraction. It supports concurrent multiple Lean 4 and Mathlib versions, provides per-request sandbox isolation, and exposes interfaces including a Python SDK, CLI, HTTP API, and a web UI with no local installation required.

AXLE’s design enables it to handle production-scale AI-driven mathematics workloads with millions of requests served, including underpinning Axiom Math’s perfect 12/12 score on the 2025 Putnam competition. Evaluations on real-world datasets such as the Goedel workbook show AXLE matches or slightly lags behind alternative long-running REPL based servers in latency and throughput but gains strong isolation guarantees. The verify_proof strict checker is about 10x faster than SafeVerify and nearly 100x faster than Comparator, two alternative strict verification tools, while maintaining very high agreement in verification verdicts. By prioritizing throughput and correctness under cooperative client assumptions, AXLE delivers the tooling needed for scalable, robust Lean 4 proof management in modern AI workflows.

Key findings

• AXLE provides 14 distinct Lean 4 metaprogramming tools enabling strict proof verification, declaration metadata extraction, semantic source manipulation, lemma extraction, and deterministic proof repair and simplification.
• AXLE’s verify_proof tool rejects candidate proofs containing sorry, non-whitelisted axioms, signature mismatches, and unsafe declarations, enforcing strict correctness beyond mere compilation.
• The service supports multi-version environments, concurrently serving multiple Lean 4 and Mathlib snapshots to enable cross-version compatibility checks and training on legacy datasets.
• AXLE runs each request with per-request isolation in sandboxed processes, preventing state leakage, crash propagation, filesystem access, and network calls between requests.
• On a 5,000-proof workload from the banach1729/goedel-workbook-lean427 dataset at concurrency 8 on AWS r7a.2xlarge, AXLE achieves 1.05s median latency, 2.09 req/s throughput, closely matching the Kimina Lean Server (0.75s, 2.13 req/s) and outperforming spawning fresh Lean processes (5.14s, 1.03 req/s).
• In comparison with other strict proof checkers (SafeVerify and Comparator) on 1,000 production verify_proof requests, AXLE’s verify_proof has median latency of 0.97s and throughput 0.43 req/s, beating SafeVerify (10.1s, 0.107 req/s) and Comparator (95.7s, 0.026 req/s).
• verify_proof reaches 100% agreement in verification verdicts with Comparator on 938 conclusive pairs and 99.3% agreement with SafeVerify on 992 conclusive pairs; discrepancies arise from name mangling in private namespaces but do not affect soundness.
• AXLE’s strict proof verification sacrifices defenses against rare environment-manipulation adversaries to gain speed and throughput in trustworthy client populations.

Threat model

The adversary is a potentially malicious or erroneous client submitting Lean 4 proof files for verification or manipulation. The adversary may attempt to evade correctness checks by inserting incomplete proofs ("sorry"), unsound axioms, or unsafe kernel-bypassing declarations. The system assumes clients will not engage in deep environment tampering such as injecting unchecked declarations bypassing the elaboration kernel. AXLE protects against standard proof-soundness failures but does not provide defenses against malicious metaprograms that install unchecked environment state or escape sandboxing to compromise other tenants.

Methodology — deep read

1. Threat Model & Assumptions: AXLE assumes an environment where clients cooperate by submitting proofs generated by AI or human-assisted tools. It defends against unsound proofs containing incomplete tactics (sorry), unsound axioms, signature mismatches, and unsafe kernel-bypassing declarations. AXLE does not protect against sophisticated environment-level attacks that bypass standard kernel checks via unchecked declarations installed by metaprograms. This trade-off prioritizes throughput and correctness under cooperative, trusted client usage rather than fully adversarial scenarios.

2. Data: AXLE’s evaluation datasets include the public banach1729/goedel-workbook-lean427 dataset, a collection of Lean 4.27.0/MATHLIB 4.27.0 formalized math proofs used in competitions, comprising thousands of proofs. Verification tests also use an internal corpus of 1,000 production verify_proof requests drawn from real client traffic demonstrating range of proof candidates encountered in practice.

3. Architecture / Algorithm: AXLE is a hosted multi-tenant cloud service implementing 14 Lean 4 metaprograms as tools operating on parsed and elaborated Lean 4 syntax. Key tools include verify_proof (strict proof verification against formal statements), extract_decls (metadata extraction), merge (semantic source merging), proof repair, and lemma extraction. The verify_proof tool performs fine-grained checks rejecting candidates containing "sorry", unsafe declarations, non-whitelisted axioms, and type mismatches, assuming the environment was built via kernel-checked elaboration. The architecture isolates each incoming request in its own sandboxed OS process to prevent side effects and state leakage. Multiple Lean 4 + Mathlib environment snapshots are concurrently supported by the same deployment.

4. Training Regime: Not applicable as AXLE itself is an infrastructure toolset rather than a learned model. However, AXLE supports AI-driven training by providing stable, scalable verification and proof manipulation.

5. Evaluation Protocol: Latency and throughput benchmarks run on AWS r7a.2xlarge and r7a.4xlarge instances with concurrency of 8 and 4 respectively, comparing AXLE against Kimina Lean Server and a baseline spawning Lean 4 per request for compilation throughput; and against SafeVerify and Comparator for strict proof verification accuracy and runtime. Performance metrics include median per-request latency, 90th percentile latency, throughput in requests/second, overall wall clock time, and accept/reject verdict agreement rates. Statistical variability is reported via latency percentiles and success rates within per-request timeouts. Evaluations cover a 5,000-proof workload and 1,000 strict verification requests, closely controlling input sets to be consistent across methods by normalizing imports.

6. Reproducibility: AXLE is publicly available as a free cloud service at https://axle.axiommath.ai, and distributed via the axiom-axle PyPI package, requiring no local Lean 4 installation. The evaluation datasets include public data sources (e.g. the banach1729 Goedel workbook) and internal production request corpora (not fully public). The code for published tools is linked, with online documentation of APIs and tool reference. The paper notes source and service URLs but does not provide a standalone reproducibility artifact bundle.

Concrete Example: A reinforcement learning agent uses AXLE’s verify_proof tool to check thousands of AI-generated candidate proofs after each rollout. Each proof candidate is sent to the service specifying the Lean 4 environment and formal statement file. AXLE executes the verify_proof metaprogram in a sandboxed worker process, rejecting candidates containing "sorry" or unsound axioms before returning a pass/fail verdict in under one second. Verified proofs then provide strong reward signals for policy updates, all at a throughput enabling practical scale training.

The modular design of 14 distinct Lean metaprograms plus concurrent multi-version environments, stateless per-request sandboxing, and cloud-based queuing/redelivery ensure the system meets demanding reliability, correctness, and throughput requirements.

Technical innovations

• A comprehensive cloud-based suite of 14 Lean 4 metaprogramming tools enables fast, strict proof verification and high-level semantic proof manipulation beyond prior compilation-only services.
• Per-request sandboxing of proofs running in isolated OS processes prevents state leakage and crash propagation, ensuring robustness under massive AI-driven concurrent workloads.
• Multi-version environment support allows serving simultaneous concurrent requests across multiple Lean 4 and Mathlib snapshots, enabling cross-version training and analysis workflows.
• verify_proof provides strict proof verification rejecting common AI-generated error modes at sub-second median latency, prioritizing scalable throughput over environment re-verification used by other strict checkers.

Datasets

• banach1729/goedel-workbook-lean427 — thousands of Lean 4.27.0 proofs from a competition-style formal mathematics workbook — public via HuggingFace
• Internal production verify_proof request corpus — 1,000 AI-generated proof candidates — private production traffic

Baselines vs proposed

• Kimina Lean Server: median latency = 0.75 s, throughput = 2.13 req/s vs AXLE: 1.05 s, 2.09 req/s on a 5,000-proof check workload
• LEAN invoked directly (no shared MATHLIB): median latency = 5.14 s, throughput = 1.03 req/s vs AXLE: 1.05 s, 2.09 req/s
• SafeVerify: median latency = 10.1 s, throughput = 0.107 req/s vs AXLE verify_proof: 0.97 s, 0.43 req/s on 1,000 strict verification requests
• Comparator: median latency = 95.7 s, throughput = 0.026 req/s vs AXLE verify_proof: 0.97 s, 0.43 req/s

Limitations

• AXLE does not support arbitrary multi-file Lean projects at request time; environments with project-specific dependencies must be pre-built and registered ahead of time.
• The system is stateless and request-scoped, so it does not support interactive proof-tree search, proof state management, or tactic-level interactions requiring long-running sessions.
• verify_proof assumes a cooperative client model and does not defend against adversarial attacks that inject unchecked declarations directly into the environment, leaving rare attack vectors open.
• AXLE only supports a fixed import header (typically import Mathlib) in its public deployments, limiting some dependency structures and extensibility during request processing.
• Evaluation is focused on competitive mathematics and AI-driven formalization workloads; robustness under highly adversarial or complex multi-user environments is not demonstrated.

Open questions / follow-ons

• How can AXLE be extended to support fully interactive proof sessions and tactic-state-level manipulations while preserving scalability and isolation?
• What architectural changes would enable secure, flexible multi-file and project dependency support without pre-built environments?
• Can strict proof verification be enhanced to defend robustly against adversarial environment manipulations while retaining throughput at scale?
• How might AXLE’s tool suite be integrated with emerging large language model agentic provers to improve end-to-end formalization workflows?

Why it matters for bot defense

For bot-defense and CAPTCHA practitioners, AXLE exemplifies building scalable, multi-tenant cloud services that safely and efficiently run untrusted or semi-trusted user-submitted code at extreme concurrency with strict correctness guarantees. The per-request sandbox isolation and automatic retries employed in AXLE provide instructive architectural principles applicable to managing isolated verification or challenge tasks in hostile environments. The multi-version environment support and semantic manipulation tools demonstrate how complex backend tooling can be exposed via standardized APIs while handling evolving dependency landscapes.

AXLE’s approach to strict proof verification balancing speed with security trade-offs may inspire bot-defense systems facing similar challenges: robust correctness checking under throughput constraints but not aiming at fully adversarial, unrestricted threat models. The service’s design trade-offs and tooling integration for AI-generated input streams also highlight patterns for defensive infrastructure in systems that must validate dynamically generated content. While formal mathematics verification differs in domain from CAPTCHAs, the engineering challenges and solutions around concurrency, isolation, and semantic correctness checking are relevant for advanced bot-defense platforms.

Cite

@article{arxiv2606_26442,
  title={ AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities },
  author={ Jimmy Xin and Alex Schneidman and Chris Cummins and Karun Ram and Srihari Ganesh and Jannis Limperg },
  journal={arXiv preprint arXiv:2606.26442},
  year={ 2026 },
  url={https://arxiv.org/abs/2606.26442}
}

Read the full paper

• arXiv:2606.26442 (abstract)
• arXiv:2606.26442 (PDF)