The Stanford Dropout Building an AI to Solve Math's Hardest Problems (www.forbes.com)

Carina Hong, a former Stanford PhD student, left academia to found Axiom Math, an early-stage startup building an “AI mathematician” that can read English-language math (textbooks, papers, journals), convert it into programmatic form, generate and verify detailed proofs, and propose new conjectures. Axiom raised $64M in seed funding (valuation reported at $300M) and assembled a small team of veterans—many from Meta FAIR—including Francois Charton (LLMs for math/theoretical physics) and others with backgrounds in safety and code generation. The startup emphasizes models that not only solve hard problems but self-check and formally test solutions, with the long-term goal of producing verifiable, research-grade mathematical discovery. The significance is twofold: technically, Axiom aims to push beyond benchmark performance (e.g., recent IMO-level results from OpenAI/DeepMind) toward autonomous, provable math research; practically, success could accelerate invention across domains that rely on complex problem solving—chip design, aerospace, finance, quantitative trading. The approach—translating informal mathematics into executable representations, generating new problems, and applying formal verification—could become a rigorous sandbox for advanced foundation models and a stepping stone toward automated scientific discovery, even as competition and the difficulty of research-level mathematics remain major challenges.