corollary

I’m still writing slides, and this will be an all-consuming activity.

In the meantime, you might like to read this neat manifesto, explaining why someone might like to mechanise mathematics. I think the computer science applications that Freek downplays are interesting too, but it’s certainly true that they are very tedious. (The art is in making them less so.)