AI, Proof and Formalization Days
Two days to examine how artificial intelligence — especially large language models — is already reshaping mathematical work, from proof-oriented reasoning to writing, idea exploration, bibliographic research, and formalization.
June 16–17, 2026
9:00 AM – 5:30 PM
ENS de Lyon, Monod campus, Lyon
This workshop aims to allow and motivate informed discussions on current uses of AI in mathematical practice. It will address both the opportunities offered by these tools and their structural limitations, while highlighting formalization with proof assistants as a scientific practice that promotes rigor, explicitness, and reproducibility.
Registration is now open:
Information and registration.
- Date: June 16–17, 2026
- Time: 9:00 AM – 5:30 PM
- Venue: ENS de Lyon, Monod campus
- Address: 46 allée d’Italie, 69007 Lyon
- Contact: ailys.coordination@ens-lyon.fr
About the workshop
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.
Main themes
- Use of LLMs for mathematical reasoning, including the (semi-)automatic construction of proofs.
- Impact on the mathematical working environment: idea exploration, argument sketches, writing support, and bibliographic research.
- Critical assessment of structural limits: hallucinations, fragile reasoning, and lack of formal guarantees.
- Formalization with proof assistants and its relation to trustworthy mathematical workflows.
Preliminary program
Day 1 — Tuesday, June 16
| 09:00 | Welcome |
| 09:30 | Introduction |
| 09:45–10:45 | Mathurin Massias |
| 11:15–12:15 | Omar Fawzi |
| 12:15–14:00 | Free buffet for registered participants |
| 14:15–15:15 | Ivan Nourdin |
| 15:45–16:45 | Frédéric Marbach |
Day 2 — Wednesday, June 17
| 08:30 | Welcome |
| 09:00–10:30 | Cyril Cohen |
| 10:35–12:05 | Xavier Roblot |
| 12:05–13:30 | Free buffet for registered participants |
| 13:30–15:00 | Theo Stoskopf |
| 15:30–16:30 | María Inés de Frutos-Fernández |
| 17:00–18:00 | Ahmad Rammal |
This schedule is provisional and will be updated as speakers and titles are confirmed.
Registration
Registration is available on the Université de Lyon event page:
Information and registration.
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)
Venue and practical information
ENS de Lyon, Monod campus
46 allée d’Italie
69007 Lyon, France
Directions to the campus:
How to reach ENS de Lyon
For questions related to the workshop, please contact
ailys.coordination@ens-lyon.fr.
The event page will be enriched progressively with the final program, abstracts, and practical information for participants.
A more detailed program page is available here: Program and abstracts.
Scientific context
The workshop is part of the scientific strategy currently being developed around artificial intelligence on the Lyon–Saint-Étienne academic site. In late 2025, the thematic institute Artificial Intelligence: uses, concepts and issues was launched to bring together research on AI and research about AI across the exact sciences, experimental sciences, social sciences, and the humanities within the member and associated institutions of the ComUE.
Its aim is to make visible, deepen, and strengthen AI-related activities across the Lyon–Saint-Étienne site, from the foundational core of AI to its many applications, uses, and broader implications. It also promotes collaborative dynamics between academic actors and with the socio-economic world.
This initiative relies in particular on the AILyS project, a consortium currently bringing together eleven higher-education, research, and health institutions of the Lyon–Saint-Étienne site around AI.