Amogh Parab

Stream: new members

[Amogh]

Hi everyone,

I'm Amogh, a recent PhD graduate from The Ohio State University. I was introduced to Lean and mathlib during the Lean3 days and had the opportunity to attend the Formalization of Mathematics workshop at SLMath in June 2023. I am now looking to actively contribute to mathlib4 and wanted to (re)introduce myself here.

My research focuses on monoidal categories, specifically categorical groups (a.k.a. 2-groups). In my thesis, Coherence and Symmetrization for Categorical Groups, I gave a construction of the free categorical groups and showed multiple coherence results. I also formalized a significant portion of this work in Lean 4, and I'm now interested in translating and extending that work into mathlib4.

To start, I’m hoping to work on formalizing categorical groups, using the Baez–Lauda paper as a main reference. I wanted to know if there is already work happening in this direction, or if this sounds like something that would be useful to have in mathlib4. While I don’t work in TQFT myself, I’ve heard from others that these structures often show up there.

I’m still new to contributing to mathlib4, so I will definitely need help as I get used to it. I have gone through the community guide for contributors. Is this the correct channel to ask workflow or lean questions? How does a typical workflow look?

Excited to get to chat with many of you!!

Thanks,
Amogh

[Kenny Lau]

@Amogh welcome, this is the correct channel, you typically want to ask around to gauge interest or get initial feedback before you spend a long time on a long PR, and typically PR's should be short (say around 200 lines) and focus on one thing at a time, that would be my advice.

I hope most importantly that you have fun on this journey!

[Yaël Dillies]

Welcome! @Kim Morrison is the canonical TQFT person, as you can see from their email :slight_smile:

[Amogh]

@Yaël Dillies Yup, already messaged them.