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 https://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…