The mathematician's toolbox.
AXLE
Infrastructure for mathematical reasoning at scale.
The Axiom Lean Engine — a hosted service for verifying and manipulating Lean proofs at scale. Safe verification faster than existing tools, plus robust primitives like verify_proof and extract_theorems that make it easy to drop a Lean runtime into a reasoning engine. It has served millions of requests inside Axiom — training our models, AxiomProver’s 12/12 on Putnam 2025, and settling open conjectures.
Axplorer
Democratizing the search for mathematical constructions.
A generative-AI tool for discovering interesting mathematical constructions — the rare, extremal objects that maximize some quantity under a constraint, like the most edges in a graph with no 4-cycle. Building on PatternBoost, it learns what the best candidates have in common and generates more — open-source, and meant for mathematicians without a background in modern AI.
