Resources

Neural theorem proving

Automated theorem proving once meant using a symbolic algorithm to search for formal proofs, but now it also includes using neural networks, reinforcement learning, and other machine learning methods to find formal or informal mathematical proofs. Machine learning is also used for autoformalization — the automatic translation of informal mathematical definitions and proofs to formal ones that can be checked in a proof assistant.

In 2024, Google DeepMind's AlphaProof reached silver-medal level at the International Mathematical Olympiad, and in 2025 several systems reached gold. Startups building Lean provers have kept pace: Harmonic's Aristotle produced formally verified IMO gold solutions, Math Inc's Gauss formalized the strong prime number theorem in three weeks, and Axiom's prover solved all twelve Putnam 2025 problems in Lean. Attention has since moved from competitions to research mathematics. First Proof, which tests AI systems on unpublished research problems, saw the best systems go from solving about two of ten problems in February 2026 to nine of ten in October.

Since May 2026, OpenAI and Anthropic have announced a string of major results, often with accompanying formalized proofs in Lean, though many have not yet been independently checked. An OpenAI model disproved Erdős's unit distance conjecture, and Levent Alpöge of Anthropic used Claude to find an explicit counterexample to the Jacobian conjecture in three variables. In September, Alpöge and Tristan Buckmaster announced Lean-verified finite-time blowup for the 3D Euler equations, and hours later OpenAI claimed a Lean-checked blowup for the 3D Navier–Stokes equations, a Millennium Prize Problem; priority is disputed. On October 6, OpenAI posted hundreds of AI-generated manuscripts, including a claimed proof of the quasi-Riemann hypothesis and a negative solution to Hilbert's tenth problem over the rationals. On October 26, it announced a Lean-checked refutation of the Exponential Time Hypothesis, which is now under independent review.

ICARM's role

At the Institute for Computer-Aided Reasoning in Mathematics, we aim to help the mathematics community make sense of these developments by evaluating and reporting on tools, and by serving as mediators between developers and the mathematics community.