Formalizing Fermat workshop

I’m organizing a workshop in London on July 6th to 10th (2026) whose goal is to work on my EPSRC-funded project formalizing Fermat’s Last theorem in Lean.

The initial aim of the project was to reduce FLT to theorems known in the 1980s, i.e. “formalize the Wiles/Taylor–Wiles papers” (although actually we are formalizing a more modern proof whose ideas go back to a strategy proposed by Khare). I have just finished giving a series of 11 lectures on the proposed proof route as part of the EPSRC Taught Course Centre which Imperial College London is part of; pdfs of the lectures are available here github.com/ImperialCollegeLondon/FLT/tree/main/2026_EPSRC_TCC_course.

However, with autoformalization becoming more and more powerful, the tech company Logos Research (who are funding the workshop) has proposed experimenting with getting AI to formalize the prerequisites which I need (and perhaps also main proof ideas themselves). Whilst autoformalization has got a lot better recently (see e.g. the second half of my talk at the recent Exeter workshop ) it still does not seem to be capable of reliably autonomously formalizing definitions correctly, or theorem statements idiomatically. My vision for the workshop is that a combination of human experts in number theory/lean plus experts in autoformalization could have a fun time experimenting with what actually can be achieved here.

For those who think “autoformalization is solved/will shortly be solved”, you could think of this workshop as a challenge to prove this. What is happening right now is that people are choosing targets for which autoformalization will work well and then saying “look we did this impressive-looking thing”. Here we’re doing something different — we’re choosing the target first, and then asking whether autoformalization is appropriate for it. The target is huge, and the answer will surely be “autoformalization is good at this part, but not very good at that part”. Given recent advances, I think it will be a very interesting project to find out exactly which parts of the (gigantic) proof of Fermat’s Last Theorem are currently suitable for autoformalization. My guess is that complex-definition-heavy parts will be bad, and parts of the proof where all definitions are already in place in mathlib and the proofs are well-documented in the human literature could well be good. But let’s see.

The deadline for applications is one week today: Friday 22nd May, 11:59pm UK time. If you are good at at least two of algebraic number theory, lean and autoformalization, please feel free to apply! The application form is here.