Hales 2017 Obergurgl

Stream: maths

[Kevin Buzzard]

I was just searching for something else (Hales' question on some physics stackexchange site about formalising Yang-Mills; I can never find it (edit : just found it)) and I ran into slides of a talk he gave in March 2017, before I was in this game. A quote from it (last page):

Formalizing statements in Automorphic Representation Theory (a branch of number theory).

This will require a great deal of work just to state the theorems that are proved: algebraic geometry (schemes, motives, stacks, moduli spaces, and sheaves), measure theory and functional analysis, algebra (rings, modules, Galois theory, homological algebra, derived categories), category theory, complex analysis (L-functions and modular forms), class field theory (local and global), Lie theory and linear algebraic groups (Cartan classification and structure theory), representation theory (infinite dimensional, spectral theory), Shimura varieties, locally symmetric spaces, Hecke operators cohomology (singular, de Rham, intersectino homology, l-adic), rigid geometry, perfectoid spaces, ...

I don't remember seeing this quote before, but I imagine that in 2017 it was in some sense written in jest. I now think that this looks like a long-term but feasible list. In three years we have made huge progress towards these goals in Lean and whilst some are clearly still a long way away, things are done, and things are in process, and I don't see why we can't go much further.

[Kevin Buzzard]

Page 4 is also worth a read :-)

[Kevin Buzzard]

On p17 Hales raises (if I understand correctly) the question as to whether categories of sheaves in HOL Light would have enough injectives.

[Bhavik Mehta]

I think it would take me about 10 minutes to show that an elementary topos has enough injectives in lean (if I'm understanding the definitions right) so I'm pretty sure we can get that result in lean

[Patrick Massot]

I like the fact that Tom's list ends with perfectoid spaces.

[Johan Commelin]

Yeah... we work from right to left (-;