AI for Mathematics

Recent years have seen striking advances in the use of Large Language Models (LLMs), combined with theorem provers and proof assistants, to support and automate mathematical discovery. In 2025, Google’s DeepMind reported gold-medal level at the International Mathematical Olympiad. Subsequently, there have been credible announcements of research-level mathematical results discovered by human-guided automated systems, or obtained with substantial AI assistance. For example, a large number of Erdos problems have been resolved in this way. Most dramatically, in May 2026, OpenAI announced a refutation of the famous Erdös conjecture on the unit distance problem with a counter example giving a new lower bound that received wide acclaim from several top notch mathematicians.

This workshop will examine the current state of the art in formal systems for mathematics and the rapidly evolving role of AI techniques in automating and augmenting mathematical research.

A central theme of the workshop will be the integration of proof assistants with LLMs. Proof assistants are software systems that allow mathematicians to formalize definitions, statements, and proofs, with every logical step checked for correctness by the system. Their use has grown rapidly, particularly for large-scale or technically intricate proofs. Notable examples are the Flyspeck project formalising Hales’ proof of the Kepler conjecture, and formalization projects by the Fields Medalists Peter Scholze and Terence Tao.
Formalizing mathematics, however, remains a highly non-trivial and laborious task. It has recently become the focus of active research at the intersection of mathematics, computer science, and AI. One important direction is autoformalization, in which mathematical text written in natural language is translated into a formal representation, often with the help of Large Language Models. Other related areas include proof synthesis, where systems suggest intermediate proof steps, and conjecturing, in which AI tools propose auxiliary lemmas or new statements that may guide a proof.

Reinforcement learning (RL) and `Neuro-symbolic AI’, have emerged as key paradigms for learning from human proofs and for discovering new ones through data-driven feedback. RL can be used very effectively in combination with proof assistants and theorem provers, providing a precise reward signal based on the success or failure of proof attempts. RL also interacts naturally with Large Language Models: LLMs can generate candidate statements or proof sketches using the intuition from neural networks, which are then checked by a proof assistant, producing feedback that is used to further improve the model.