JOURNÉES IA ET RAISONNEMENT MATHÉMATIQUE : IA, preuve et formalisation

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. I will introduce the Transformer architecture for sequence modelling, in particular its Attention mechanism. I 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.

I 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] .

In this talk, I 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. We 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.

I will share my 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, I 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.

15:30 María Inés de Frutos-Fernández
Formalizing the universal divided power algebra in Lean
Formaliser l'algèbre universelle à puissances divisées avec Lean

I 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.

Horaires de la journée

Lien pour suivre la visio conférence : https://visio.numerique.gouv.fr/khp-wppk-mwh

Comité scientifique :

• 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)

Construction d’une stratégie scientifique de site autour de l’intelligence artificielle à Lyon Saint-Étienne

Dans le cadre de la stratégie scientifique déployée sur le site académique Lyon Saint-Étienne, l’Institut Thématique Intelligence Artificielle : enjeux, concepts et usages et a été lancé en cette fin d’année 2025. Il rassemble des activités en IA et sur l’IA issues des sciences exactes, expérimentales, sociales et humaines au travers de l’ensemble des établissements membres et associés de la ComUE impliqués dans ces thématiques. Son objectif est de faire connaître, approfondir et renforcer les activités du site Lyon Saint-Étienne sur l’IA. Sont ciblés tant le cœur fondamental de l’IA que ses nombreuses applications, ses enjeux et ses usages.

L’Institut Thématique en IA promouvra les dynamiques collaboratives entre acteurs académiques et avec le monde socio-économique. Son ambition pour le territoire : soutenir la structuration et le développement de la recherche, de l’innovation et l’offre de formation en IA sur Lyon Saint-Étienne.

Il s’appuie notamment sur le consortium AILyS, qui fédère aujourd’hui onze établissements de l’enseignement supérieur, de la recherche et de la santé du site Lyon Saint-Étienne autour de l’IA : Centrale Lyon, l’ENS de Lyon, l’ENTPE, les Hospices Civils de Lyon, INSA Lyon, Mines Saint-Étienne, VetAgro Sup, les universités Claude Bernard Lyon 1, Lumière Lyon 2, Jean Moulin Lyon 3 et Jean Monnet Saint-Étienne.

 

Inscriptions aux journées IA et mathématiques :

Inscriptions fermées.