Keep pulling the thread on Carina Hong.
Axiom Math has raised $64 million in funding.
Axiom's AI system solved 9 out of 12 problems on the Putnam exam, a score that would have won the competition against 4,000 human participants in the previous year.
It took AWS's automated reasoning team five years to manually formalize the memory isolation component of their hypervisor.
Axiom's mission is to build a self-improving reasoning engine that combines generation and verification, starting with the domain of mathematics.
Axiom's AI system uses the formal language Lean to ground its natural language processing capabilities, combining deterministic tooling with probabilistic systems.
Karina Hong predicts that AI will transform mathematics by allowing mathematicians to work at a higher level of abstraction, using AI as a "diligent grad student" to formally prove their intuitions.
Axiom believes that simply scaling informal language models is not a viable path to achieving Artificial General Intelligence (AGI) in mathematics.
In the hardware industry, verification teams can be three to four times larger than design teams, and the verification process for a chip can take up to three years.
Stanford's automated reasoning lab, led by Professor Clark Barrett and supported by DeepMind and AWS, is developing CSLib to formalize undergraduate computer science literature in the Lean language.
Karina Hong believes it will take a long time for AI to match the intellectual capabilities of the top 0.0001% of human mathematicians like Terence Tao.
Axiom identifies code migration and proving the functional equivalence of legacy and new code as a key commercial use case for its formal verification technology.