project presentations

Stream: LftCM22

[Kevin Buzzard]

@Heather Macbeth or indeed anyone, is there a complete list of the project topics which were presented on Friday, and of people involved? I think there were 9? presentations and then @Thomas Browning did an impromptu last one on normal closures. PS Thanks a lot Thomas :-)

[Heather Macbeth]

@Kevin Buzzard I wrote it down, yes.

• symplectic group: Matej Penciak, Fabien Cléry, Moritz Doll
• word metric on groups: Jim Fowler
• formally étale morphisms: Jackie Lang, Judith Ludwig
• H-spaces: Florent Schaffhauser, Ángel González Prieto, Filippo Nuccio
• divided powers: Antoine Chambert-Loir, María Inés de Frutos Fernández
• orthonormal bases: Daniel Packer
• cstar-algebras: Jon Bannon, Jireh Loreaux
• power series for square root: Tyler Billingsley, Phil Wood
• closed immersions: Sam van Gool, Jake Levinson
• normal closures: Thomas Browning

It'd be good to have a complete list, so feel free to remind us here of projects you worked on even if you were too shy to present on Friday! (Looking at you, Hopf fibration group ...)

[Kevin Buzzard]

Oh yes! @Daniel Hast definitely did something nontrivial with number fields (a spin-off from the quadratic fields project, for which they may not be enough API right now). Was there any progress on the chromatic number of the plane?

[Jon Bannon]

I have to say although my "presentation" was more an off-the-cuff screenshare combined with some disorganized remarks, I am quite proud of how much I was able to learn last week and to have had the chance to show it to this wonderful and friendly community. Thanks again for a great experience! And special thanks to Jireh for his time and attention. (He is an absolutely fantastic Lean mentor...much more so than my progress indicated!) :tada:

[Patrick Massot]

Jon, it was a very nice experience to see your enthusiasm along the week. I really hope you'll stick around and contribute great things to mathlib and using Lean for teaching.

[Jon Bannon]

:smile: Indeed, Patrick, I will stick around and do exactly the things you hope. :+1: It may take me a bit to get up to speed, but LCFTCM 2022 really gave me a fantastic boost.

[Dustin Mixon]

Kevin Buzzard said:

Oh yes! Daniel Hast definitely did something nontrivial with number fields (a spin-off from the quadratic fields project, for which they may not be enough API right now). Was there any progress on the chromatic number of the plane?

There was progress on the chromatic number. The "of the plane" part is still in progress.