new members introduction

Stream: new members

[Marek]

hello everyone! just want to introduce myself, my name is Marek, I am a PhD student in Physics with Computer Science background, I accidentally found Lean and I became curious about it and decided to join this community and observe a bit to see if it would be the right tool for my projects

[Oscar Matemb ⚛️]

Hey, I am from Catonsville, MD. I want to learn more about lean and implement it in my comp sci work.

[Derrik Petrin]

Hello! I'm a student in the CS masters program at University of Washington and a software engineer at Wizards of the Coast (I work on the rules engine for MTG Arena). I've been wanting to fill some gaps in my math education, and one of the CS PhD students pointed me to LADR for more advanced linear algebra. I also recently took the graduate programming languages class at UW, which is taught in Coq, and really enjoyed working with a proof assistant.

I'd like to use Lean as an aid for working through LADR—any advice on how to use Lean effectively along with a text like this? I'm currently going through the natural number game to pick up differences b/w Coq and Lean, and I found a post here from a few months ago with a discussion about LADR. It sounds like the necessary structures and lemmas are pretty built out in mathlib and I just need to be judicious with leaning (heh) on those as much as I can.

[Sven Manthe]

Hello. I'm a PhD student in logic at the University of Bonn (my advisor is Philipp Hieronymi), and also have a computer science background from my Bachelors. I'm not sure yet about how much and what for I'll use Lean

[Yaël Dillies]

Hello! I think we're in the same room right now. :grinning: