Mini Lean Workshop

Natural Numbers Game Exercises Empty Editor Cheat sheet with many tactics A list of topics in Mathlib

More or less recent recommended reading:

Communal blog: Proofs and Prompts
Kevin Hartnett: "The Proof in the Code" (Book)
Breaking Math: The Math Is True. But Is It True True? — based on an interview with Talia Ringer
Marianna Girlando, Fabrizio Montesi: Library-Grade Modal Logic (arXiv, 3 October 2026)