Final FLT lecture of term

Stream: FLT

[Kevin Buzzard]

I've been giving a (quite disorganized) course on FLT this term, but as I mentioned last week I finally got sick of Teams and I'll give the last lecture on Zoom, link here (same as last week's). The lecture is possibly at 2024-12-09T13:00:00Z -- that should be 1pm London time and 8am Pittsburgh time tomorrow Monday, let me know if I screwed up, because parts of my computer think it's GMT and other parts think it's Eastern US time right now (I'm in Pittsburgh -- the lecture is coming live from the Hoskinson center).

In the first hour I will go through a maths proof that a space of quaternionic modular forms is finite-dimensional, and then people can just go ahead and formalize issues in the second hour. I'm also sick of using an iPad to deliver lectures so I'm going to try pdf slides, which I'll post here after the lecture (I've not written them yet). I'll be assuming that you know what the adeles of a number field $K$ are but most of the time I'll only be using the fact that they're a locally compact topological $K$-algebra.

[Kevin Buzzard]

Here are the notes for the lecture; they have not been "blueprintized", and they have also not been turned into sorried Lean statements, which actually should probably be the next step before I blueprintize.

hoskinson_talk.pdf

Next steps: me or someone else starts writing Lean code corresponding to the claims in the lecture which are not formalized, and opening issues. I see, how about this for a workflow: first I add a bunch of issues but don't assign them to the project, and then I write the sorries and add the issue numbers, and then I put the issues on the dashboard, and then I write the blueprint last.

[Ruben Van de Velde]

You might want to share the handout pdf :)

[Kevin Buzzard]

As Ruben points out, here is a far more convenient version to read:
hoskinson_talk.pdf

[David Michael Roberts]

Just bung the pdf into an AI, Kevin, it will turn it into a blueprint, right? :stuck_out_tongue_wink:

[David Michael Roberts]

FWIW https://xenaproject.wordpress.com/2024/12/11/fermats-last-theorem-how-its-going/

Very interesting wrinkle there.

[David Michael Roberts]

And of course it was

Brian Conrad

who found the fix