For now I'm just learning math with it! Currently I'm going through https://github.com/teorth/analysis https://github.com/teorth/analysis (Tao's Lean companion

For now I'm just learning math with it! Currently I'm going through https://github.com/teorth/analysis 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 https://github.com/gaearon/analysis-solutions).