AI for Mathematics

This Institut Mittag-Leffler workshop examines the state of the art in formal systems for mathematics and the fast-changing role of AI in automating and augmenting mathematical research. Large language models combined with theorem provers and proof assistants have recently reached gold-medal level at the International Mathematical Olympiad and contributed to research-level results, including the resolution of many Erdős problems and a 2026 counterexample to Erdős's unit distance conjecture. A central theme is integrating proof assistants with LLMs: proof assistants check every logical step of formalised definitions, statements and proofs, as in the Flyspeck formalisation of Hales's proof of the Kepler conjecture and formalisation projects led by Peter Scholze and Terence Tao, but formalisation remains laborious. The workshop covers autoformalisation (translating natural-language mathematics into formal representations), proof synthesis, AI-driven conjecturing of lemmas and statements, and reinforcement learning and neuro-symbolic methods that learn from human proofs and use proof-checker feedback as a precise reward signal.