| ▲ | joachimma 5 days ago | |
Terrence Tao is apparently in the process of converting the exercises from his "Analysis I" book into Lean. https://terrytao.wordpress.com/2025/05/31/a-lean-companion-t... | ||
| ▲ | majikaja 5 days ago | parent [-] | |
This is cool I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks. | ||