Comment by danabramov
3 days ago
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).
very cool. btw, I also love that "sorry" is the "any" equivalent in Lean