While the baby is sleeping, I'm having fun working through the Lean natural numbers game wwwf.imperial.ac.uk/~buzzard/xena/…
In reply to @christianp
So far, I'm repeating the background reading of the PhD I never finished. I'm glad I didn't finish, because Lean makes it superfluous
In reply to @christianp
If anyone wants to pay me to write "Proof assistants for babies", I'm open to it