| ▲ | danabramov 11 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). | ||
| ▲ | kevinqi 11 days ago | parent [-] | |
very cool. btw, I also love that "sorry" is the "any" equivalent in Lean | ||