{"id":"arxiv:2606.26442","kind":"preprint","title":"AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities","authors":["Jimmy Xin","Alex Schneidman","Chris Cummins","Karun Ram","Srihari Ganesh","Jannis Limperg"],"author_count":6,"year":2026,"published":"2026-06-24","venue":null,"cited_by":0,"doi":null,"arxiv_id":"2606.26442","nct_id":null,"source_url":"https://arxiv.org/abs/2606.26442","archive_url":"https://space-kitty.com/papers/arxiv:2606.26442","updated":"2026-06-24","pmid":null,"pmcid":null,"openalex_id":"W7166018589","pdf_url":"https://arxiv.org/pdf/2606.26442","abstract":"We present AXLE (Axiom Lean Engine), a cloud service for Lean 4 proof manipulation, extraction, and verification. Recent progress in AI for mathematics -- reinforcement learning pipelines, agentic proving workflows, dataset curation -- demands Lean 4 tooling that scales to millions of requests while remaining correct and robust; existing infrastructure offers parallel compilation but not scalable proof verification, higher-level proof manipulation, multi-version support, or per-request isolation at the throughput modern AI workflows require. AXLE provides 14 Lean 4 metaprogramming tools spanning strict proof verification, declaration metadata extraction, semantic source manipulation, deterministic proof repair and simplification, and lemma extraction. The service runs as a multi-tenant cloud deployment with per-request isolation and concurrent support for multiple Lean 4 and Mathlib versions, accessible via a Python SDK, command-line interface, web UI, MCP server, and raw HTTP API. AXLE is publicly available and free to use at https://axle.axiommath.ai and via the axiom-axle PyPI package, with no local Lean 4 installation required. It has served over 500 million requests to date and is the underlying infrastructure for Axiom Math's proving efforts, including its 12/12 score on the 2025 Putnam competition.","abstract_license":"CC0-1.0 (arXiv descriptive metadata)","license":null,"is_open_access":false,"retracted":false,"peer_reviewed":false,"categories":["cs.LO","cs.AI"],"details":null,"provenance":"arxiv","attribution":"Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.","topics":[{"slug":"ai-mathematics","name":"AI for Mathematics & Formal Proof","domain_slug":"math-cs"}],"cited_in_dossiers":[]}