Axiom, a startup founded just seven months ago, has achieved a notable milestone by solving all 12 problems from the prestigious Putnam mathematics exam, scoring 8/12 within the time constraints and 12/12 overall—outperforming top undergraduate competitors and rival AI systems. The Putnam exam, legendary for its difficulty with a median human score typically at zero or one point, has long served as a benchmark for mathematical reasoning. While this accomplishment follows a familiar pattern of AI systems beating humans at elite competitions, CEO Carina Hong argues the real significance lies not in the achievement itself but in what it reveals about AI's path to artificial general intelligence. Hong contends that coding ability—demonstrated by systems like Claude Code—represents a necessary but insufficient milestone toward AGI. She frames the challenge as an "informal bottleneck" in AI development, where current systems excel in domains with clear formal specifications but struggle with the intuitive, unstructured reasoning that characterizes human expertise. Drawing parallels to mathematician Srinivasa Ramanujan, Hong describes how formal verification and proof generation allow AI systems to "scale brilliance" by making intuitive insights explicit, verifiable, and buildable by others. This philosophy underpins Axiom's focus on verified AI—using formal verification techniques and languages like Lean to create mathematical proofs that can be rigorously checked and communicated, rather than relying on informal pattern matching.