This summer school offers an introduction to proof assistants for mathematics and its applications in programme certifications. It covers several recent techniques, such as homotopy theory or the interactions with large language models.
The summer school is composed of five lectures and three talks. Each lecture (2x1h30) will be complemented by 2 hours of tutorials. It is primarily intended for the students of the graduate program "Mathematics and interactions: research and interactions" of the University of Strasbourg but is also accessible to any interested PhD student or researcher. As space is limited, priority will be given to PhD students. This event is supported by the Interdisciplinary Thematic Institute IRMIA++.
It will take place from 31 August to 4 September 2026 in the IRMA conference room at the University of Strasbourg.
Lectures
Introduction to type theory, Loïc Pujet (Université de Strasbourg)
Abstract
Introduction to categorical logic, Thibaut Benjamin (Université Paris-Saclay)
Formal languages derived from lambda calculus and type theory provide rich and expressive languages for formalizing a range of mathematical results. Variants with diverse degrees of expressiveness allow us to work within “mathematical worlds” of varying degrees of rigidity. At the same time, category theory provides a generic framework for axiomatizing such mathematical worlds. My goal is to explore the existing correspondences between these formalisms through the concepts of semantics and internal languages. The simplest manifestation of this duality lies between algebraic theories and Lawvere theories. It then extends to richer correspondences: lambda calculus and cartesian closed categories, essentially algebraic theories and categories with finite limits, generalized algebraic theories and clans...
Introduction to synthetic homotopy theory, Axel Ljungström (University of Nottingham)
One of the most revolutionary ideas in modern theoretical computer science is that types -- the basic building blocks of any system of type theory -- can be interpreted not as sets or data structures, but as topological spaces (up to continuous deformation), i.e. the objects studied in the fields of homotopy theory and algebraic topology. In this course, we'll make practical use of this rather surprising connection and explore some of the basics of traditional homotopy theory/algebraic topology, working entirely in the language of type theory. We will see how, by adding two features to type theory called _higher inductive types_ and _univalence_, we obtain a version of type theory called _homotopy type theory_ that is strong enough to prove statements about e.g. the fundamental group (roughly, the group of continuous loops) of the circle.
Introduction to Lean: Formalizing Mathematics with Mathlib, Xavier-François Roblot (Universite Claude Bernard Lyon I)
Abstract
Introduction to transformers and their application to proof assistants, Theo Stoskopf (Inria, Lyon)
Large language models have recently become powerful tools for producing text, code, and increasingly formal proofs. In this course, we will first introduce the transformer architecture, the architecture behind modern LLMs, and explain the ideas that make it effective: attention, token-based prediction, large-scale pretraining, and test-time compute. We will also discuss some of the specific challenges involved in training such models on text and formal data. We will then turn to the interactions between LLMs and proof assistants. Proof assistants offer an interesting setting for language models: they provide a programming language, large libraries of verified mathematics, and a reliable checker that can validate or reject generated proofs. We will survey current uses of LLMs in this area. Finally, during the tutorial session, participants will experiment with ways in which LLMs can act as assistants for proof assistants.