Comment by joachimma

3 days ago

Terrence Tao is apparently in the process of converting the exercises from his "Analysis I" book into Lean.

1 comment

joachimma

This is cool

I guess intros based on the structure of mathlib could work for people who haven't published their own textbooks.