Introducing myself: Tom Kranz

Stream: new members

[Tom Kranz]

I should've probably done this before necro'ing a two-year old thread, but better late than never.
I'm Tom (he/him) and working as a research associate (if there are any fellow Wissenschaftliche Mitarbeiter around, please help me find a good translation – I seem to have introduced myself wrongly for quite some time) at the Theoretical CS deparment at the University of Potsdam, Germany. I've been interested in using proof assistants for teaching and was infected with Lean last summer at the Proof Assistants for Teaching summer school in France. I would be very excited to be able to contribute something to this community and was wondering if, when I have a suggestion for a question in mind, I should just blurt it out or leave it to the pros. I've been unable to find an etiquette guide upon a cursory search, so any pointers would be appreciated as well. :)

[Yaël Dillies]

Blurt it out! We have a good-first-issue label on the mathlib repo: https://github.com/leanprover-community/mathlib4/labels/good%20first%20issue. Feel free to pick up anything from there

[Yaël Dillies]

... and here are a few more on the old repo: https://github.com/leanprover-community/mathlib/labels/good-first-project

[Tom Kranz]

Great, I've added my two cents to a Zulip thread now – exciting stuff! The Turing machine composition looks enticing, but I think I'll stick to the Regular expression equivalence and really dig into what y'all have done before, first.

[Tom Kranz]

Oh and maybe on my background: I've helped with teaching Intro to automata theory and formal languages for five years now (eight if you count my assistant time) and have dabbled in institutions (describing the mappings between logics) for my Master's thesis. Not really any research experience, though.