Chris Grossack

Stream: new members

[Chris Grossack (they/them)]

Hey all! I think I'm doing this right? I tried using Zulip in the category theory server a while ago, but it always feels a bit unintuitive, haha. Hopefully I figure it out, because I'm really interested in learning LEAN.

[Chris Grossack (they/them)]

I guess as a first question (though I'm not sure if it should go here or elsewhere), the thing that finally got me on zulip is an undergrad who wants to do a formalization project with me. I'm happy to oblige, and I think this will be a great opportunity for me to learn LEAN myself! I don't have a good guess for what will be both easy and useful, though...

One idea that I had (knowing my strengths and this student's interests) is Lawvere theories, or Essentially Algebraic Theories, as well as (possibly) their associated dualities (lawvere duality/gabriel ulmer duality). A glace through mathlib doesn't turn anything up, but I don't really know how to look through it efficiently, so I may be missing something.

What do people think about this? And is there a good place to go for advice? Obviously I'll want to practice some formalization basics first, haha.

[Johan Commelin]

Hi and welcome! I can confirm that we don't have Lawvere theories yet. But we should have all the prerequisites to get started.
The best place to go for advice is either #new members or #maths, I think.

[Chris Grossack (they/them)]

Fantastic, thanks for the welcome ^_^. I'll go ahead and ask again on #maths, then!