Challenges coming from Hales' Big Proof slide

Stream: mathlib4

[Kevin Buzzard]

hales_slide.png

I just ran into the slide which Tom Hales put up in 2017, with his list of stuff which needed to be formalised just to state the results in his area of expertise. Looking at them seven years on, we're doing pretty well!

Notable definitions which we don't have: motives (needs a theory of varieties, which we don't have), moduli spaces (there was progress made at the AIM meeting but it would be nice to see a roadmap), class field theory (progress is being made here by Maria Ines and Filippo, and I will hopefully be running something in 2025 specifically on this, although nothing is confirmed yet), locally symmetric spaces (probably we have the prerequisites for this now) and rigid geometry (probably via Huber's foundations). But we really have knocked off a bunch of stuff on this list; it's funny to think that in 2017 this was complete science fiction!

The slide appears 35 minutes into Hales' talk here.

We should probably do algebraic varieties at some point :-)

[Adam Topaz]

what does "motives" mean here?

[Kevin Buzzard]

I'm assuming it means "one of the standard definitions of pure motives" and although humanity can't prove they're all equal, I'm pretty sure that we can't currently state any of them in Lean!