update

Stream: FLT

[Kevin Buzzard]

For the first year of the project, we focussed a lot on a bottom-up theorem, that certain spaces of automorphic forms are finite-dimensional, and we are largely done with the proof. I have been quite bad at reviewing PRs recently (I'll get to why later on) but I had a go over the weekend and I've realised that we have done almost all of the adeles part of the argument and almost all of the finiteness part of the argument; what's left is some technical results about haar characters.

More recently I have turned to thinking about a top-down argument, which involves a lot of technical Galois representation stuff and modularity lifting theorems, and I've mostly been keeping myself to myself. I'm going to give 8 2-hour lectures at Imperial next term (Jan-March 2026) where I'm really going to push forwards with this stuff and actually write a blueprint; it has somehow taken me a very long time to flesh out the proof into something coherent which I understood all the details of, but I think I am there now modulo a modularity lifting theorem which is well-documented in the literature.

The thing that has been a big distraction for me recently is that I want to prove the main theorems of local class field theory and I've been working on this in private with a group of people who attended the Oxford Clay workshop on the topic. We have nearly finished the proof and this has become my main priority. I really hope to get back to bottom-up FLT soon and get the finiteness result sorry-free. I am naively hoping that I can get bottom-up FLT back on track and class field theory over the line by Christmas. Then in the new year I'm going to focus on top-down FLT.

There might be some money for jobs at Imperial, perhaps for people who are experts in the number theory related to top-down FLT and/or number theorists interested in AI. If there's anyone out there who would be able to move to Imperial quickly (e.g. by Jan) then could they let me know by DM? It's a pretty niche job description so I am not optimistic I'll find anyone appropriate but I thought I'd ask.

[Mario Carneiro]

Kevin Buzzard said:

I'm going to give 8 2-hour lectures at Imperial next term (Jan-March 2026) where I'm really going to push forwards with this stuff and actually write a blueprint

Will these lectures be recorded?

[Kevin Buzzard]

Only if I secretly record them, which I could do...

[Ryan Smith]

Next best thing, will you post your notes for the lectures?

[Ruben Van de Velde]

Or: will your students?

[Kevin Buzzard]

ok I'll upload the pdf slides for the lectures to the repo.

[Kevin Buzzard]

Brief update from me:

1) CI is failing and I don't know why.

✖ [8112/8112] Building FLT/FLT:docs (10s)
info: Documentation indexing
trace: .> /home/runner/work/FLT/FLT/.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 index --build /home/runner/work/FLT/FLT/docbuild/.lake/build
error: no such file or directory (error code: 2)
  file: /home/runner/work/FLT/FLT/docbuild/.lake/build/doc/references.bib
Some required targets logged failures:
- FLT/FLT:docs
error: build failed
Error: Process completed with exit code 1.

I hit "rerun job" a few times but this doesn't seem to fix it.

2) Right now I am very much focussed on giving my course, which is a regular mathematics course on FLT in which I assume without proof everything known in the 1980s. There will be 8 2-hour lectures of which I have given 3 and will be giving another one today. The course will run until mid-March. I will then attempt to turn the course notes (which are appearing here https://github.com/ImperialCollegeLondon/FLT/tree/main/2026_EPSRC_TCC_course ) into a blueprint and then a Lean skeleton, and then there will be plenty of new things to work on. But right now I am basically working 100% on what I think is the most important issue for the project going forwards, which is actually writing down a complete and detailed roadmap for the route to FLT modulo 1980s which I am taking. For those aware of the Stanford course which Taylor gave last year; I am basically going through the same material but my emphasis is sometimes different. For example Taylor might spend several hours talking about a result which was known in the 1980s which I will skip; conversely Taylor will sometimes dismiss various arguments as standard but, even if they are, I will give careful details if I know of no 1980s reference.

3) I am reluctant to bump the repo to the new Lean rc v4.29.0-rc1 for reasons explained elsewhere (downstream repos are being encouraged not to bump); however I am happy to bump to v4.28.0 so I will be merging FLT#859 some time after today's FLT lecture. Many thanks @Ruben Van de Velde for the bump.

[Ruben Van de Velde]

Re 1) I've seen a few comments going around related to references.bib. Let me see if I can find them

[Ruben Van de Velde]

FLT#860 might/should help

[Rémy Degenne]

For 1) I had the same issue in the Brownian motion project, I updated docgen-action to the lastest commit, and then CI worked. I just did that, so perhaps CI is not really fixed and will fail during the next run, I don't know.

[Ruben Van de Velde]

Looks like it worked