Thomas Murrills

Stream: new members

[Thomas Murrills]

Hi all! I'm new to Lean, and I'm excited to start formalizing! I have some familiarity working in Agda and type theory in general, so I'm hoping to jump right in and familiarize myself with Lean's syntax and unique features. (Simply having classes seems very exciting, for one!)

I figured I'd primarily work in Lean4 instead of Lean3. I'm still planning to learn the basic syntax of Lean3 so that I can read source code and (potentially) help with the port to mathlib4, but figure I may as well write all new code in Lean4. Does this seem like a reasonable choice?

Looking forward to meeting you all! :)