Wednesday lectures

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

My feeling is that things are going faster than expected, which is great. Adam and I are really hoping that you can prove AB5 for condensed abelian groups by the end of the week. Adam will talk about things related to this today, and I'll do warm-up from 9 to 10, talking about abelian categories in Lean, finite biproducts, and filtered colimits.

[Scott Morrison]

Since when is formalisation faster than expected? I thought the planning fallacy was baked into Lean's axioms.

[Adam Topaz]

We probably won’t have everything “sorry-free”, but a decently complete skeleton should be done by the end of the week!

[Kevin Buzzard]

People are working hard!