AI, Proof and Formalization Days

This talk is meant as a broad introduction to the field of LLMs, aiming to provide 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, including text tokenization, next-token prediction, model training, and fine-tuning.

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 the 2023 Nature paper on FunSearch.

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.

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 \(I\) in a commutative ring \(R\), a divided power structure on \(I\) is a collection of maps \(\gamma_n : I \to I\), indexed by the natural numbers, which behave like the family \(x^n/n!\), but which can be defined even if division by factorials is not defined in \(R\). The triple \((R, I, \{\gamma_n\})\) is called a divided power algebra. To any \(R\)-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.

We present AutoformBot, a multi-agent system for autoformalizing mathematical textbooks in Lean 4. AutoformBot orchestrates LLM agents equipped with formal verification tools, dependency-aware scheduling, and collaborative version control to translate informal textbook prose into machine-checked definitions and proofs. Applied to 26 open-access textbooks, it produces Atlas, a verified Lean 4 library containing over 45,000 declarations and 500,000 lines of code. These results suggest that autoformalizing substantial parts of graduate-level mathematics at scale is becoming technically and economically feasible, opening new perspectives for the verification of both human- and machine-generated mathematics.