I formalized lemmas regarding geometrically irreducibility of a ring, and its relation to tensor products. And shown this coincides with the same notion in scheme world.
This workshop is aimed primarily at PhD students with an interest in formalising results from algebraic geomery using the Lean proof assistant. Participants will work in teams on formalisation projects designed by our guest speakers.