A bottom-up approach to formalisation in the FLT project

Abstract: This talk will describe a collaborative multi-author project to develop foundational material required for the formalisation of the proof of Fermat’s Last Theorem. The culmination of this project is a sorry-free proof that a certain space of automorphic cusp forms is finite-dimensional. We will report on the overall status of this project, with a particular focus on the adele ring sub-project, as well as the ongoing efforts to upstream our results to mathlib.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026