The n-Category Café

I’d like to draw your attention specifically to the following paragraph:

It reminds me of playing board games on the iPad or on a computer: it’s not the same as playing in real life, but one of the distinct advantages is that you don’t have to remember all the rules yourself. If you can’t play a tile in a particular location in Carcassonne, the app simply won’t let you put it there. When you try to take a second face-up locomotive card in Ticket to Ride, the app doesn’t allow it. Play the app enough times, and the rules gradually become second nature, without having to consult the rulebook or have an experienced player walk you through it.

Something about this rang a bell when I read it, but it took a little while for me to figure out why. Part of it, of course, is that all of mathematics is, from a certain point of view, a game. (This is especially evident under a formalist philosophy of mathematics.) And when we learn any new part of mathematics, we have to practice working with its rules until they become “second nature” to us. That’s why the best textbooks include exercises.

But eventually I realized that this also sounds very much like a description of my experience using computer proof assistants to do mathematics in (homotopy) type theory! Indeed, I’ve heard at least one type theorist refer to Coq as “the world’s best computer game”. And I don’t mean just that it is extremely addictive and can keep you up late at night (both of which I can vouch for personally). I mean that it does precisely the same thing for type theory that DragonBox does for algebra: you don’t have to remember all the rules yourself.

Coming from a background in classical mathematics, type theory can be hard to wrap your head around. Things that were difficult become easy, and things that were easy become difficult (or false). Often things that are obviously the same to you are not actually identical, and a term that looks perfectly all right doesn’t actually typecheck. It’s extremely easy to make errors when doing type theory on paper or in LaTeX; but if you do it with a proof assistant, then you simply aren’t allowed to make any mistakes. (That doesn’t mean it’s easy to achieve what you want; following the rules doesn’t guarantee by any means that you’ll prove your theorem. Just like DragonBox will happily let you manipulate an equation correctly to your heart’s content, but you still may not get any closer to solving for $x$.) And eventually, the rules do start to become second nature. Without Coq to hold my hand, I would only understand type theory at a fraction of the depth that I do (though I still have a ways to go to be a real type theorist).

Are there other aspects of higher mathematics that can be “gamified”? Perhaps string and surface diagrams?

Maybe one day 5-year-old children will be learning homotopy type theory on their iPads.