Formal Verification and Verified AI for Mathematical Reasoning at Scale

axiom_math · Research & Academia · 2025 · source Agentic: yes · promotional bias: med · source-backed · extracted with prompt 0.5.6 (schema v2)

Generated from extraction.json — do not edit by hand. Every claim cites verbatim source evidence; stated means the quote directly asserts the claim, implied means it supports it indirectly.

Problem

Domain: formal mathematical reasoning and verified code generation

Axiom Math is building a verified reasoning system for mathematics and software-like proof tasks, where LLM-generated reasoning must be grounded by Lean proof checking rather than accepted as informal natural language output.

Constraints:

• formal math requires executable proof objects, not just plausible natural-language reasoning
• the system depends on Lean data and existing formal definitions in MathLib-like libraries
• complex proof goals need decomposition and backtracking rather than single-shot generation
• auto-formalizing informal problem statements lacks grounding when the problem has not been solved
• hardware and verification markets may require all-or-nothing correctness rather than partial credit

Architecture

Axiom Prover is an ensemble of post-trained models built on foundation models with coding and natural-language capability, then adapted with Lean proof data and reinforcement learning for formal mathematics. The system decomposes proof goals into subgoals, learns to backtrack, uses Lean verification as a correctness signal, and is paired with Axiom Lean Engine tools and an API for validation, manipulation, repair, and integration into external coding or proof workflows.

Diagram confidence: reconstructed (reconstructed from prose).

flowchart LR
  problem-specification[Problem specification]
  post-trained-proof-models[Post-trained proof models]
  recursive-proof-planner[Recursive proof planner]
  lean-proof-verifier[Lean proof verifier]
  axiom-lean-engine-tools[Axiom Lean Engine tools]
  verified-generation-api[Verified generation API]
  problem-specification --> post-trained-proof-models
  post-trained-proof-models --> recursive-proof-planner
  post-trained-proof-models --> lean-proof-verifier
  recursive-proof-planner --> lean-proof-verifier
  recursive-proof-planner --> axiom-lean-engine-tools
  lean-proof-verifier --> axiom-lean-engine-tools
  lean-proof-verifier --> verified-generation-api
  axiom-lean-engine-tools --> verified-generation-api
  verified-generation-api --> problem-specification
  verified-generation-api --> axiom-lean-engine-tools

Components

Data flow

A problem enters as an informal math, code, or verification task. The system uses foundation-model reasoning adapted on Lean proofs to propose a formal path, recursively decomposes the proof goal into subgoals, invokes Lean and AXL-style verification/manipulation tools to validate or repair proof attempts, and either returns formally verified proof/code or reports that the task remains too hard. Verified outputs and proof-validation scores can then feed post-training or downstream workflows.

Why this architecture

The architecture uses formal verification because Axiom argues that Lean gives a grounding and reward signal that informal proofs cannot provide, making verified generation a performance strategy rather than only a compliance tool. The API/tooling layer exists because setting up and operating Lean verification is specialized and non-trivial, especially at scale.

Models used: Axiom Prover · open-source foundation models · Lean · Axiom Lean Engine

Scale

• Axiom reports solving 187 of 189 Code Verifier problems, or 99%, with code and proof.
  “we actually recently with no modification to the Pan M system we saw a 99% out of the 189 problems we solved 187.”transcript, stated
• Axiom Prover was observed scaling proof trees from 40 nodes to 4,000 nodes.
  “Uh we have seen it scale from 40 notes to 4,000 notes.”transcript, stated
• Axiom Lean Engine is described as a set of 14 proof validation and manipulation tools.
  “Axel is currently, I think, 14, uh, like, such tools, uh, starting from verified proof”transcript, stated
• Formal verification for ASIC projects is described as having design-to-verification ratios around 1:3 or 1:4 in size and duration.
  “the industry standard for design to verification in ASIC ASIC project is like one to three one to >> One to three and to four, correct. Both in size and in duration.”transcript, stated
• The company was about 30 people at the time of the interview.
  “we're currently about like 30 people now, right?”transcript, stated

Alternatives considered (roads not taken)

purely informal math reasoning with natural-language proofs

Rejected because: Axiom argues informal reasoning lacks the executable verification and reward signal needed for verified generation and math AGI.

verification as only a compliance or hallucination-reduction tax

Rejected because: The system is framed around performance gain, collaboration, and compounding intelligence rather than only reducing mistakes.

letting every frontier lab build a dedicated formal verification team

Rejected because: Axiom positions verification as a specialized API or partner capability that other labs can call rather than staffing rare Lean meta-programming expertise themselves.

LLM-based repair as the only way to fix broken Lean

Rejected because: AXL includes dedicated repair tools intended to make broken-Lean-to-good-Lean repair cheaper and more straightforward.

Patterns

fine-tuning-adaptation (model-adaptation)

Axiom adapts foundation models with continued training, fine-tuning, and reinforcement learning on Lean proof data for formal mathematics.

eval-driven-development (evaluation)

Lean proof checking and AXL verification tools act as executable evaluation and reward signals for proof correctness.

tool-use-orchestration (tooling)

The system wraps Lean verification in AXL tools and an API so models and developers can validate, manipulate, and repair formal proofs.

human-in-the-loop-gate (oversight)

Auto-formalization still needs human review because formalizing an unsolved statement lacks an automatic grounding signal.

rag-retrieval (knowledge-management)

The case highlights retrieval and provenance as production problems for mathematical discovery, where equivalent or indirectly solved results are hard to find.

Tradeoffs

Use verified generation instead of purely informal reasoning.

Chose Lean-grounded formal proofs and verification over natural-language proof claims from informal LLMs.

Rationale: Formal proof objects can be checked and used as reward signals, while informal proofs create mixed objectives and weaker RL feedback.

Expose verification as a specialized API and partner layer.

Chose Axiom API and AXL tools over every customer or frontier lab building an in-house formal verification team.

Rationale: Lean meta-programming talent is rare, infrastructure is non-trivial, and verification can be composed into existing LLM workflows.

Build from open-source or off-the-shelf base models with domain post-training.

Chose post-training and RL over Lean data over training a frontier foundation model from scratch.

Rationale: Axiom can start from models with language and coding ability, then specialize them for formal math where Lean supplies correctness signals.

Bridge informal and formal reasoning rather than choosing one extreme.

Chose a hybrid high-level/low-level formal reasoning stack over completely informal or completely formal-only approaches.

Rationale: The source argues that code-like formal systems can transfer reasoning while keeping verification at the low-level proof boundary.

Gotchas (what bit them)

Formal math performance shifts by domain coverage.

Root cause: The prover depends on existing Lean definitions and MathLib infrastructure, so domains with weaker formalized foundations are harder.

Resolution: Treat domain formalization coverage as a prerequisite and expect better generalization where definitions already exist.

Auto-formalization has weak grounding before a problem is solved.

Root cause: Unlike proof checking, translating an informal statement into a formal spec often lacks executable input-output feedback.

Resolution: Use tests or human review where available, and separate formalizing proofs from formalizing unsolved statements.

Proof obligations can dwarf the original program.

Root cause: Formal verification may require many proof lines for each line of executable code, and scaling laws for proof complexity are uncertain.

Resolution: Decompose proofs, use tools and repair utilities, and avoid assuming proof overhead stays small as programs grow.

Mathematical retrieval can misclassify solved problems as open.

Root cause: Prior solutions may exist under equivalent formulations, indirect extensions, old papers, or distributed sources such as forums.

Resolution: Invest in knowledge bases and retrieval that reason over equivalence and provenance, not just direct title or keyword matches.

Hardware-style verification gives no partial credit.

Root cause: Some target domains require perfect proof rather than probabilistic confidence or mostly correct behavior.

Resolution: Use formal verification where the domain demands all-or-nothing correctness and keep informal approaches for lower-stakes software.

Evaluation

Axiom evaluates through formal proof checking, proof/code benchmarks, proof-tree complexity, and comparisons against informal LLM and formal prover baselines.

Metrics: 99% on 189 Code Verifier problems, solving 187 · Axiom Prover proof trees scaled from 40 nodes to 4,000 nodes · comparison against GPT pass-one and iterative results, and against other formal math systems around 11-12% · summary-reported Putnam score of 120/120 versus 110 best human and 103 best informal LLM

Outcomes

• Axiom reports 99% performance on Code Verifier with 187 of 189 problems solved.
• The system reportedly handled proof trees growing from 40 nodes to 4,000 nodes.
• Axiom Lean Engine was released as a free suite of proof validation and manipulation tools and saw early Lean community usage.
• The summary reports a 120/120 Putnam result and open research progress across multiple mathematical domains.

The company is about 30 people, raised $200 million at a $1.6 billion valuation, released 14 Lean tooling capabilities, and targets verification markets with hundreds of humans and thousands of software licenses on single verification problems.