Zulip Chat Archive

Stream: new members

Topic: Thomas Murrills

Thomas Murrills (Sep 26 2022 at 21:23):

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! :)

Last updated: Dec 20 2023 at 11:08 UTC