[kevinqi]

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?

[danabramov]

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).

[kevinqi]

very cool. btw, I also love that "sorry" is the "any" equivalent in Lean