Axiom Math reports automated Lean proofs as AI mathematics race accelerates

Axiom Math said its Axiom Prover recently produced several solutions to open research problems that were fully automated and formalized in Lean without human intervention. The company also said it set a world record on the parity of the partition function.

The update follows a rapid contest over bounded gaps between primes: Julia Stallemann improved the record from 246 to 240, Axiom Math reached 212, and OpenAI Astra later reached 186. Axiom said it expects similar races with OpenAI and Anthropic, while acknowledging that competitors can overtake its results quickly.

Axiom described AI as a tool that amplifies mathematicians and said mathematical questions such as the still-unsolved Riemann hypothesis remain. It expects scientific research to thrive over the next six to eight months, but that outlook is a prediction rather than a confirmed result.