Reading up on Mathlib
2 deep · digging since may 29
- How Terry Tao Became an Evangelist for AI in Math
Terry Tao champions combining human insight, AI, and the Lean proof assistant to enable massive, verified mathematical collaborations.
- All Lean Books and Where to Find Them
A personal guide lists and reviews nine Lean 4 books, offering subjective opinions and suggested learning paths.