Reading up on Mathlib
3 deep · digging since may 29
- Human mathematicians are being outcounterexampled
AI tools have rapidly generated and formalized counterexamples to longstanding conjectures such as Erdős’ unit distance, Grothendieck’s group scheme problem, and the Jacobian conjecture, showing machines now out‑counterexample humans.
- 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.
