as someone who hasn't seen Lean before but was curious from alphaproof, love the intro! curious if you can mention what you're working on in Lean?

For now I'm just learning math with it!

Currently I'm going through https://github.com/teorth/analysis (Tao's Lean companion to his textbook) and filling in the `sorry`s in the exercises (my solutions are in https://github.com/gaearon/analysis-solutions).