Zulip Chat Archive

Stream: maths

Topic: Hales 2017 Obergurgl

view this post on Zulip Kevin Buzzard (May 24 2020 at 20:00):

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.

view this post on Zulip Kevin Buzzard (May 24 2020 at 20:00):

Page 4 is also worth a read :-)

view this post on Zulip Kevin Buzzard (May 24 2020 at 20:03):

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

view this post on Zulip Bhavik Mehta (May 24 2020 at 20:18):

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

view this post on Zulip Patrick Massot (May 24 2020 at 20:19):

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

view this post on Zulip Johan Commelin (May 25 2020 at 04:58):

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

Last updated: May 18 2021 at 07:19 UTC