Carina Hong

Carina Hong is the founder of Axiom, identified as its CEO in a June 2026 Latent Space interview article. She treats an AI mathematician as a starting point for broader reasoning: a system that generates full proofs, proposes new questions and builds on existing mathematical knowledge. Her central public argument is that verification enables intelligence to accumulate—“scaling brilliance, compounding brilliance”—rather than merely catching mistakes.[2][1]

In her Thought Economics interview, published in December 2025 and updated in March 2026, Hong outlined four components: a prover that produces proofs with intermediate steps; a conjecturer that proposes questions for the system to attempt; a knowledge base that consults existing results and supports searches for counterexamples; and auto-formalization, which translates natural-language mathematics into machine-verifiable Lean proofs. She considers auto-formalization at least as important as proving because it connects the other components. This is her stated architecture and research direction.[2]

Hong envisions people using informal reasoning and intuition to guide exploration, with formal systems grounding those ideas through verification. Discoveries made at the formal level can then inform higher-level intuition. She also identifies a practical obstacle: scarce Lean training data weakens auto-formalization, while weak auto-formalization makes it harder to generate better training data. Conjecturing presents another open problem because proposed statements do not immediately supply verifiable proofs as feedback.[2]

In June 2026, Hong expressed the belief that verified generation is necessary for AGI. She also highlighted the difficulty of specifying what a system should establish: “Anything that can be specified can be proven. Humans are bad at specifying everything we want.” The statement captures her emphasis on specification as part of the verification problem.[1]

Axiom’s January 8, 2026 proof release credits Hong in leadership alongside Hugh Leather and Shubho Sengupta, with Chris Cummins and GasStationManager separately credited as prover leads. Axiom reported that AxiomProver solved all 12 problems from the December 6, 2025 Putnam exam in Lean, receiving them section by section from an official proctor after each section began. Eight solutions were completed within the exam time; the full set took longer.[5]

The team’s account illustrates why formal proof generation involves more than reproducing human explanations. For problem A5, an induction argument that could be sketched in a few paragraphs became an unoptimized 2,054-line Lean formalization that Axiom reported took 518 minutes to generate. For geometry problem B1, the system produced a symbolic proof that the company’s mathematicians needed a hand-drawn diagram to understand. These were team-reported system results, with Hong credited for leadership.[5]

The supporting infrastructure includes AXLE, the Axiom Lean Engine, publicly released on March 5, 2026. It exposes tools for exploring, validating and manipulating mathematical proofs; Axiom says its primitives were used in model training and the Putnam work.[6]

Hong describes entering company leadership from an individual-contributor research background and learning through feedback, trial and error. Her recruiting principle is to hire people who can surpass her in ability and execution, while she keeps improving. She describes Ken Ono’s mentorship and working with François Charton at the intersection of AI and mathematics as inspiring.[2]

Before Axiom, Hong’s work spanned mathematics and AI research. A first-generation college student, she graduated from MIT in 2022 with a double major in mathematics and physics, then earned an Oxford neuroscience master’s with dissertation distinctions and conducted AI and machine-learning research at the Gatsby Unit. These earlier studies provide context for the research background she brought to leadership.[3][4][2]

MIT’s November 2022 announcement named Letong (Carina) Hong as the forthcoming recipient of the 2023 AMS-MAA-SIAM Morgan Prize for proving results and solving conjectures in combinatorics, number theory and probability. At that time she was at Oxford as a Rhodes Scholar for China and had previously served as president of MIT’s Undergraduate Mathematics Association.[4]

Hong thanked undergraduate advisors Pavel Etingof for kindness and support, Scott Sheffield for introducing her to random surfaces, and Henry Cohn for teaching and encouragement during setbacks. Her subsequent 2024 Knight-Hennessy cohort profile identifies her as Carina Letong Hong and describes her pursuing a Stanford law degree, providing legal aid to low-income workers and using economic analysis to advocate law enforcement reform.[4][3]