Oliver Nash: Root systems and root data in Mathlib

Stream: Lean Together 2025

[Jireh Loreaux]

A thread for discussion about this talk.

[Oliver Nash]

Slides from my talk

[Eric Wieser]

That was an excellent story about evolving definitions, thanks!

[Chris Birkbeck]

Nice talk!

[Oliver Nash]

slides.pdf

[Rob Lewis]

I'm glad this was recorded! I often find myself trying to convince people that definitions are the hardest part of formalizing, now there's a video to point to :grinning:

[Johan Commelin]

I particularly like that the final definition is quite a bit more readable than the 3 versions before it.

[Michael Bulois]

Lie theoretist here, very nice talk explaining both the maths and the formalization issues. Appreciated it very much

[Oliver Nash]

Thanks!

[Paul Schwahn]

Also from me: nice work! What I've gathered from the talk is that we now have an adequate definition of root systems/root data. You also mentioned the obligatory next steps: writing API for root systems. How much progress has been made on this? And to take it further: are we ready to classify simple root systems (over fields etc.), for example?

[Johan Commelin]

Classification of simple root systems is very much on the radar!

[Johan Commelin]

I really hope we can get it done before the summer break.

[Oliver Nash]

Yes, as I mentioned in the talk, most of the theory has been developed by @Scott Carnahan. E.g., thanks to his work we already have things like docs#RootPairing.coxeterWeight_mem_set_of_isCrystallographic

The march is definitely on to the classification of reduced finite crystallographic root systems over a field of characteristic zero. In fact I think if #20667 and #20384 are merged we might be ready just to follow the standard path.

[Oliver Nash]

Anyone is most welcome to help!

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/ZPPDktjL1Lw