Comment by joachimma

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...