<p>apparently my idea of what to do on a big pain day is to learn Lean 4 from the reference manual</p>