Axiom Math Develops 'Verifiable' AI That Proves Its Answers
Axiom Math has developed an AI system, the "Axiom Prover," which is reportedly the first to autonomously solve open research conjectures with fully verifiable proofs. Founder Carina Hong explained the system uses formal proof languages to build AI that can prove it is correct, addressing the core problem of AI hallucinations. The hybrid approach combines natural language reasoning with formal verification, aiming to create more trustworthy AI assistants for complex tasks.
Axiom's founder, Carina Hong, is a 24-year-old Stanford PhD dropout and award-winning mathematician who previously studied at MIT and Oxford. The company, founded in March 2025, quickly attracted top AI researchers from Meta and Google Brain, securing a $64 million seed round at a valuation of around $300 million. The Axiom Prover uses a formal proof language called Lean, which acts as a strict referee for mathematical logic. This system combines a creative neural network that explores potential solutions with a symbolic engine that ruthlessly checks every logical step, a hybrid approach designed to eliminate AI "hallucinations" by ensuring every part of the proof is verifiable. This technology marks a significant shift from AI that produces plausible-sounding text to systems that can formally prove they are correct. Historically, formal verification has been incredibly laborious; for example, verifying the 8,700-line seL4 microkernel required 20 person-years of effort. AI-driven provers aim to make this level of certainty accessible for mainstream software engineering. To benchmark its progress, Axiom Prover autonomously solved all 12 problems of the 2025 Putnam Competition, widely considered the world's most difficult undergraduate math exam, where the median human score is typically 0 or 1. The system has also solved multiple long-standing open problems, including a conjecture on Riemann surfaces and two Erdős problems. While the immediate focus is mathematics, the underlying goal is to create verifiable reasoning for high-stakes industries. Potential applications include formally verifying the correctness of software and hardware, securing cryptographic protocols, and ensuring the reliability of algorithms in quantitative finance and aerospace design.
