Axiom Math (legal name: Axiom Quant Inc.) builds an AI system designed to solve and generate advanced mathematics — and to formally verify every step of its reasoning. Its core product, AxiomProver, takes a math problem, proposes a proof, and outputs it in Lean, a formal programming language where every logical step is machine-checked and guaranteed correct. This eliminates the hallucination problem inherent in standard LLMs. Beyond solving problems, the system proposes novel conjectures — mathematical statements never previously proven — meaning it can generate genuinely new knowledge, not just regurgitate training data. A second tool, Axplorer, democratizes pattern discovery for working mathematicians. The company is also expanding its "Verified AI" approach to software code generation: any AI-written code function can be proven to always return the correct answer and to be free of hidden vulnerabilities. Buyers include academic mathematicians, quantitative finance firms, and eventually any enterprise that needs provably correct AI-generated software. Founded March 2025 by Carina Hong (Stanford PhD dropout, Morgan Prize winner) and Shubho Sengupta (former Meta AI researcher).