Axiom Math raises $200M to build mathematical superintelligence using formal verification — scored a perfect Putnam

Summary

Axiom Math raised $200M to build mathematical superintelligence by combining post-training reasoning with formal verification in Lean, a language designed for machine-checkable proofs. The company, founded by MIT math and physics graduate Carina Hong, scored a perfect 120 out of 120 on the Putnam competition last December, while the best-performing large language model scored 103.

Hong frames math as a sandbox for building verifiable AI systems. Unlike informal reasoning, mathematical proofs can be checked step-by-step in Lean, which enables efficient reinforcement learning with absolute right-or-wrong feedback. The company has scaled from the Putnam win to solving research-level problems that professional mathematicians find challenging, with transfer to code verification as well.

Axiom has solved Putnam questions ranked harder than IMO problems, questions other AI systems have not solved. The International Mathematical Olympiad's problem six, famously unsolved by both OpenAI and Google, required visual insight—noticing a floor tiling pattern—that no AI had found. Hong notes the joke about this problem: no AI could solve it because they "were not at the Australian airport." Axiom has not yet achieved a perfect IMO score, but Hong emphasizes progress on questions of extreme hardness by mathematical competition standards.

Hong positions math as a horizontal bet analogous to how coding proved to be a broader lever than initially expected when Anthropic began focusing on it in 2024. She argues that verified AI powered by formal methods will become foundational infrastructure for verifying all AI-generated code and reasoning. The framing is not about catching mistakes or erasing hallucinations, but about enabling AI agents and human-AI teams to compound superintelligence. She invokes mathematician Ramanujan learning proof writing from Hardy and Littlewood and becoming more powerful as a result, viewing AI as capable of similar leverage by turning intuitive reasoning into formally verifiable theorems.

On mechanistic interpretability, Hong draws a distinction. Rather than opening the black box of internal model behavior, verified AI focuses on trusting outputs once generated. Formal verification allows mathematicians to operate at higher abstraction levels, with Lean tactics handling low-level deduction and freeing mathematicians to focus on high-level navigation and accelerate discovery timelines. This reasoning advantage could flow to applied science.

The $200M will fund compute and hiring. Hong emphasizes building a world-class team and recruiting people interested in program verification.

Axiom's bet rests on the premise that mathematical reasoning combined with formal verification becomes a critical path to superintelligence verification. The leap from math excellence to general verification infrastructure is stated clearly but not yet proven in practice.