Scaling Past Informal AI: Formal Verification as the Path to Math AGI

The central tension Carina Hong exposes is that informal AI systems, no matter how large, hit a ceiling when reasoning must compound reliably. Current language models generate plausible-sounding math but cannot guarantee correctness, and RL on informal outputs gives weak training signals because the reward is fuzzy. Axiom Math‘s thesis is that scaling intelligence past this barrier requires formal verification baked into the training loop, not bolted on as a post-hoc checker.

Concretely, Axiom uses the Lean theorem prover as both the environment and the reward signal. Their system generates candidate proofs, Lean verifies them mechanically, and that binary pass/fail outcome becomes a dense, unambiguous reward for RL. This approach produced a perfect 120/120 on the 2024 Putnam exam, outperforming every other AI system and the best human competitor at the time. Hong argues that verified generation creates a compounding loop: better proofs train better models, which produce harder-to-verify proofs, which push the system further. The company’s $200M Series A at a $1.6B valuation, just seven months in with 30 people, reflects investor conviction that formal methods are the path to math AGI rather than a niche academic tool.

For a builder, the takeaway is that verification is not just a safety or reliability concern—it is a scaling property for reasoning. Informal systems inherently degrade in reliability as they grow; formal ones can compound. The hard open problem Hong flags is the specification gap: we still need humans to write the conjectures and definitions that the system proves. The practical move is to watch infrastructure like the Axle API (their open Lean-at-scale layer) and benchmarks like Verina (code with proofs), because the real bottleneck is no longer model size but the quality and density of verified training data. If you want AI that can build on its own discoveries, informal reasoning alone will not get you there.