MATRIX-MFO Tandem Workshop: Machine Learning and AI for Mathematics - Oberwolfach Report 43/2025

Aug 2, 2026

Upload by Ophelia

MATRIX-MFO Tandem Workshop examined how modern machine learning can accelerate mathematical discovery while retaining rigorous proof standards. The program addressed three directions: AI-driven progress on difficult problems, mathematical understanding of AI predictions, and deep-learning models for automated theorem proving. Discussions covered search-space navigation and conjecture generation, integration of large language models with formal systems such as Lean/mathlib, and collaborative/autoformalization workflows. Emphasis also included reinforcement learning and search for proof generation, alongside curated supervised data for high-quality reasoning.

LanguageEnglish

CategoryTechnology

FormatPDF

Pages28

Reading Time1 h 11 min

AccessFree to download

Introduction by the Organizers

Workshop focus and three research angles

Machine learning for discovery and search spaces

AI predictions and mathematical understanding

Automated theorem proving with formal systems

Mathematisches Forschungsinstitut Oberwolfach Report No. 43/2025 DOI: 10.4171/OWR/2025/43 MATRIX-MFO Tandem Workshop: Machine Learning and AI for Mathematics Organized by Fran¸cois Charton, Paris Jan de Gier, Melbourne Amaury Hayat, Paris Julia Kempe, New York Geordie Williamson, Sydney 21 September – 27 September 2025 Abstract. This workshop explored how modern machine learning can both accelerate mathematical discovery and preserve rigorous standards. It focused on three angles: using AI techniques to help mathematicians make advances on challenging problems; using mathematics to understand AI predictions; and using deep-learning models for automated theorem proving. Key discussions included using machine learning as a tool for constructing interesting mathematical constructions and navigating in mathematical search spaces, to uncover conjectures and high-quality examples (e.g., sphere packings via DiﬀuseBoost, combinatorial objects via AlphaEvolve); Integrating Large Language Models (LLMs) with formal systems (e.g., Lean/mathlib) to create scalable, certiﬁable AI-based automated theorem prover; Collaborative formalization (e.g., the Carleson theorem project), autoformalization for high-quality supervised data, and reinforcement learning/search methods for proof generation and algorithmic reasoning. Mathematics Subject Classiﬁcation (2020): 68T07, 03B35, 68V15, 68V20, 68Q32, 68T05, 68Q25 . License: Unless otherwise noted, the content of this report is licensed under CC BY SA 4.0 . Introduction by the Organizers Having intelligent computers able to solve complicated problems on their own has been a sci-ﬁ fantasy for almost as long as computers have existed. The progress of Artiﬁcial Intelligence (AI), and in particular Deep Neural Networks, in the last 20 years has made this a reality for a number of tasks and has revolutionized some 2324 Oberwolfach Report 43/2025 areas such as vision [26, 29] or translation and natural language processing [?, 25] . While it is usually conceivable that an AI could translate words, play chess, or process data as well or better than humans, it has often been hard to believe that they could perform abstract mathematics on their own. Nevertheless, over the last few years, works on AI for mathematics have been developing at a rapid pace and AI techniques have enabled new discoveries in mathematics [9, 12, 31] in knot theory [21, 9, 15], representation theory [3], partial diﬀerential equations [28], dynamical systems [1], control theory [18, 2] and many others. Interestingly, in many cases the neural networks involved are relatively small, far from large language models. This may indicate that neural networks exploit yet unknown structures and representations, and that understanding their mode of operation may shed new light on the underlying mathematical problems. On the other hand, applications of Reinforcement Learning (RL) and Large Language Models (LLMs) to automated theorem proving have also made drastic progress in the last six years [24, ?, 22, ?, 7, 32] The tandem workshop Machine Learning and AI for Mathematics, organized by Fran¸cois Charton (Paris), Jan de Gier (Melbourne), Amaury Hayat (Paris), Julia Kempe (New-York), Geordie Williamson (Sydney), aimed at discussing how AI methods can help mathematician advance mathematics. It was well attended, with over 40 participants. It focused on three angles: • Using AI techniques to help mathematicians make advances on hard problems; • Using mathematics to understand AI predictions; • Using deep-learning models for automated theorem proving. Since neural networks are notoriously good at spotting and learning weak signals and hidden structures, even in complex problems, they can be trained to suggest solutions to hard problems or counterexamples to conjectures, in the manner of an “artiﬁcial intuition”. In this workshop we focused on several related lines of research. One considers problem solving

FAQs

What three main themes did the workshop focus on?

The workshop focused on: using AI to help mathematicians make advances on hard problems, using mathematics to understand AI predictions, and using deep-learning models for automated theorem proving.

How can machine learning support mathematical discovery according to the organizers?

Neural networks can learn weak signals and hidden structures, training to suggest solutions to difficult problems or counterexamples to conjectures, helping explore search spaces and uncover conjectures and high-quality examples.

What role do formal systems play in automated theorem proving discussed in the workshop?

Formal proof assistants such as Coq, Isabelle, and Lean express mathematics with logical precision and verify proofs. The workshop also discussed integrating large language models with formal systems (e.g., Lean/mathlib) to enable scalable, certifiable automated theorem proving.

Aug 2, 2026

Upload by Ophelia