Axiom, a startup valued at $1.6B, is betting that formal verification using the Lean proof language is the key bottleneck to AGI progress. CEO Carina Hong argues that AI systems relying on informal proofs hit a ceiling, while verified generation enables compounding intelligence — each formally proven result becomes a trusted building block for future training and inference. Axiom achieved 99% (187/189) on the Verina code-with-proof benchmark, compared to OpenAI o3's 4.9%, and solved all 12 Putnam exam problems. The core thesis: formal proofs provide a much stronger RL reward signal than statistical methods like GRPO, improving sample efficiency and enabling a compounding corpus of verified knowledge. Hong argues no path to AGI exists without verified generation.
