Building the Reasoning Engine at Axiom (axiommath.ai)

Axiom announced a “reasoning engine” aimed at autonomous mathematical discovery by combining hierarchical planning, formal verification, and self-play. The program leverages three converging trends—neural networks that now scale into reasoning, maturing proof assistants like Lean that make proofs executable programs, and LLMs that reliably generate code (including formal specifications)—to autoformalize informal math into machine-checkable proofs and autoinformalize formal proofs back into human-intelligible insight. The stack behaves like an interactive, bidirectional compiler: translate intuition to formal code, verify or refute it, then lift machine-found patterns back into high-level conjectures. Technically, the engine centers on a conjecturer–prover loop operating over a knowledge base of formalized mathematics. Formal verification supplies binary ground truth and a scalable reward signal; failed proofs yield counterexamples that teach the system; successful proofs expand the formal corpus, improving subsequent search and conjecturing. LLMs act as strong priors over the huge action space, while hierarchical planning orchestrates moves across abstraction layers. The result is a self-improving system—“AlphaGo for mathematics”—that can generalize out-of-distribution, surface lemmas humans miss, and accelerate the pipeline from discovery to application. If successful, this approach could transform scientific modeling across domains (from protein folding to quantum theory) by making mathematical creativity and verification massively parallel and machine-scalable.