Walk around Mathlib: every building is a file, every hill as high as the mathematics is deep. Follow Lemma the owl along real chains of theorems and watch them light up.