Trebor Huang

Stream: new members

[Trebor Huang]

Hi everyone! I've asked a few newcomer questions here, but never introduced myself.

I'm an undergrad student in Tsinghua University. Previously I wrote quite a bit of Agda, primarily concerning type theoretic and constructive math. I also code in Haskell.

I'm still trying to get used to Lean's syntax, but hopefully that'll be quick. I'm interested in doing metaprogramming and porting to Lean4. And, as a math undergrad, I would also like to see what I can contribute to mathlib.

This community is awesome and helpful, I've been learning a lot here!