Shaunticlair Ruiz (self-introduction)

Stream: new members

[Shaunticlair Ruiz]

Hello! Apologies if I'm doing this wrong, I couldn't easily find a discussion for centralized self-introduction, so I'm just making my own discussion (thread? Still getting used to Zulip terminology after skimming)

My name is Shaunticlair, I'm a USAmerican who just finished his Master's in Neuroscience+Computer Science at MIT. I realized near the end of my Master's program that I'm excited about formal verification in general, and decided to get started with Lean. I'd say my background is primarily in Machine Learning, Computer Science, and Mechanical Engineering. I'm also interested in education; I wrote a machine learning textbook as a supplement to the intro ML class at MIT.

I've worked through the natural number game, set theory game, and I'm currently almost done with the Mechanics of Proof textbook. I'll probably start Mathematics in Lean next. My rigorous mathematics background is admittedly pretty weak; I've only partly studied Real Analysis. I've spent some spare time self-studying a little bit of metalogic philosophy, because I think it's cool and I wanted to get a stronger grounding in what proofs are. My goal is to get more familiar with Lean, and then start using it as my workspace for going through some undergrad math classes. Not sure what my end goal is yet, maybe contributing to creating LLMs that use Lean to validate their own outputs, to make sure that the educational materials it creates are accurate (highly ambitious tbh, but it's a goal).

Looking forward to meeting and speaking with you all! I feel vaguely intimidated by my limited mathematics background, but I can always work on it.