IA and Mathematics Days: AI, Proof and Formalization Days – Workshop on mathematical practice in the age of generative tools

Two days to examine how artificial intelligence – especially large language models – is already reshaping mathematical work, from proof-oriented reasoning to writing, idea exploration, and bibliographic research.

Deux jours pour s’informer et échanger sur l’usage actuel de l’intelligence artificielle – en particulier des modèles de langage (LLM) – dans la pratique mathématique.

Image

© kjpargeter / Freepik

This two-day meeting aims to encourage discussion and exchange on the current use of artificial intelligence — in particular large language models (LLMs) — in mathematical practice. It will examine concretely what these tools can already contribute to mathematics: first, within mathematical reasoning itself, especially through the (semi-)automatic construction of proofs; and second, within the working environment of mathematicians, through tools for exploring ideas, sketching arguments, drafting text, and conducting bibliographic research.

The workshop will also analyze the structural limitations of these technologies — errors, fragile chains of reasoning, and the absence of guarantees — together with the conditions for their responsible and informed use. Particular attention will be given to formalization with proof assistants, viewed both as a scientific practice fostering rigor, explicitness, and reproducibility, and as a possible semi-automatic verification layer within AI-assisted proof generation.

More broadly, these two days are intended to open a space for reflection on the evolution of mathematics in the age of generative tools. 

Programme

16th of June – Retour d’expérience

9:00 Accueil

9:45 Mathurin Massias
An introduction to Transformers and LLMs
Introduction aux modèles Transformeurs et grands modèles de langage

This talk is meant as a broad introduction to the field of LLMs, aiming at providing the audience with a common basis for the rest of the workshop. Mathurin Massias will introduce the Transformer architecture for sequence modelling, in particular its Attention mechanism. He will then present the broader use of Transformers as Large Language Models (LLM), prensenting the concepts of text tokenization, next token prediction, model training and finetuning.

11:15 Omar Fawzi
New combinatorial constructions via program search with LLMs
De nouvelles constructions combinatoires par recherche de programmes avec les grands modèles de langage (LLMs) 

Omar Fawzi will describe the FunSearch methodology (short for searching in the function space), a procedure based on pairing a pretrained LLM with a systematic evaluator and illustrate how it can be used to search for interesting combinatorial constructions, such as large cap sets. The talk will be mostly based on [Nature2023] .

12:15 Repas (buffet offert)

14:15 Ivan Nourdin
The future of mathematics in the age of AI
L’avenir des mathématiques à l’ère de l’Intelligence Artificielle

In this talk, Ivan Nourdin will look back at the “Malliavin-Stein experiment”, conducted last September with C.-P. Diez and L. Da Maia, to explore what AI was able to bring to mathematical research at that time. Ivan Nourdin will then discuss the mathematical advances enabled by AI since then, before reflecting more broadly on what the future of mathematics might look like in the age of AI.

15:45 Frédéric Marbach
Struggles and Sparks: Daily Math with LLMs
Défis et Percées : les maths au quotidien avec les grands modèles de langage

Frédéric Marbach will share his experience and personal habits for using LLMs in everyday mathematical research: searching for bibliography, learning new theories, proving theorems, auditing proofs, and reviewing papers. Starting with examples from control theory, he will specifically review the process of proving a theorem achieved through 86 conversations with recent models. The talk will address various ways of interacting with both poor and excellent models, via the web, APIs, and IDEs.

17th of June – Vérifier, formaliser

08:30 Accueil

09:00 Hands-on (Travaux pratiques) avec Cyril Cohen (formalisation en Rocq)

10:35 Hands-on (Travaux pratiques) avec Xavier Roblot (formalisation en Lean)

12:15 Repas (buffet offert)

13:30 Hands-on (Travaux pratiques) avec Theo Stoskopf (auto-formalisation)

15:30 María Inés de Frutos-Fernández

Formalizing the universal divided power algebra in Lean
María Inés de Frutos-Fernández will present a formalization in the proof assistant Lean of the universal divided power algebra. This is an analogue, in the theory of divided powers, of the classical algebra of polynomials. It is a crucial tool in the development of crystalline cohomology, and it is also used in p-adic Hodge theory to define the crystalline period ring.

Given an ideal II in a commutative ring RR, a divided power structure on II is a collection of maps γ_n:I→Iγn:I→I indexed by the natural numbers which behave like the family xⁿ/n!xn/n!, but which can be defined even if division by factorials is not defined in RR; the triple (R,I,{γ_n})(R,I,{γn}) is called a divided power algebra. To any RR-module, one can associate a universal divided power algebra.
While working on this formalization project, we uncovered an error in Roby’s 1965 construction of the universal divided power algebra, which we repaired by providing an alternative proof inspired by the ideas in Roby’s paper. The work discussed in this talk is joint with Antoine Chambert-Loir.

17:00 Ahmad Rammal 

Presentation of AutoformBot and ATLAS. AutoformBot is an open-source multi-agent system that was used for building ATLAS, an Autoformalized Textbook Library At Scale, in Lean 4, by translating informal textbook prose into machine-checked definitions and proofs.
Rammal et al. (2026). Formalizing Mathematics at Scale. arXiv:2605.29955. https://doi.org/10.48550/arXiv.2605.29955.

Scientific committee

• Frédéric Déglise (UMPA)
• Stéphane Gaussent (ICJ)
• Philippe Malbos (ICJ)
• Véronique Maume-Deschamps (ICJ)
• Sophie Morel (UMPA)
• Filippo Nuccio (ICJ-LIP)

An event organized in the context of the Lyon Saint-Étienne scientific strategy

The workshop is part of the scientific strategy currently being developed around artificial intelligence on the Lyon Saint-Étienne academic site. Late 2025, a Thematic Institute in Artificial Intelligence: uses, concepts and challenges was launched to bring together research on AI and research about AI across exact sciences, experimental sciences, social sciences, and humanities carried out by all members and associated members of Université de Lyon (ComUE).

It aims to make visible, deepen, and strengthen AI-related activities across Lyon Saint-Étienne, from the foundational core of AI to its many applications, uses, and broader implications. It also promotes collaborative dynamics between academic stakeholders and with the socio-economic world.

This initiative relies in particular on AILyS, a consortium currently bringing together 11 higher education, research, and health institutions in Lyon Saint-Étienne around AI.