AI, Proof and Formalization Days

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.

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.