## June 18, 2012

### The Gamification of Higher Category Theory

#### Posted by Mike Shulman

I found the following article when John posted about it on Google Plus:

Go read it; I’ll wait for you below the fold.

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.

Posted at June 18, 2012 9:21 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2535

### Re: The Gamification of Higher Category Theory

(After I realized this myself, I noticed that someone else had also commented on the similarity at the end of the article.)

Posted by: Mike Shulman on June 18, 2012 9:31 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

I also play with kseg from time to time; alas, it doesn’t yet have an interface for verifying coincidences, but it’s lots of fun, extensible (though its polymorphism is very limited) and, like the others, remembers the rules for you.

Posted by: Jesse McKeown on June 18, 2012 11:01 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

Thanks for the link! I remember using Geometer’s Sketchpad back when I was in high school, but I haven’t seen kseg before.

Posted by: Mike Shulman on June 18, 2012 11:05 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

Formalism aside, certain results in mathematics have benefited from a game theoretic approach. I was reminded of Lachlan’s game theoretic methods in degrees of unsolvability.

Posted by: Barry Cunningham on June 19, 2012 1:14 AM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

I was wanting to make a game based/using on higher categories for a long time, but I was thinking in term of RPG. And in that case AI is the problem. May be I’ll give it another try, or may be just make it as puzzle…

Posted by: Serge on June 19, 2012 4:48 AM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

Eric Finster seems to have gamified opetopic pasting diagrams.

Posted by: Jesse McKeown on June 22, 2012 5:19 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

How do I win?

Posted by: Mike Shulman on June 22, 2012 5:25 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

There are no game pieces yet, just the board.

Posted by: Eric Finster on June 24, 2012 1:15 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

It’s not exactly a ‘game’, but Aleks Kissinger, Alex Merry, Ben Frot, Bob Coecke, Lucas Dixon, Matvey Soloviev and Ross Duncan are developing Quantomatic, a computer tool that manipulates string diagrams according to user-defined rewrite rules:

Recent graph-based formalisms for computation provide an abstract and symbolic way to represent and simulate quantum information processing. Manual manipulation of such graphs is slow and error prone. This project employs a formalism, based on monoidal categories, that supports mechanised reasoning with open graphs. This gives a compositional account of graph rewriting that preserves the underlying categorical semantics.

We are using open graphs as the representation for a generic ‘logical’ system (with a fixed logical kernel) that supports reasoning about models of compact closed category. A salient feature of the system is that it provides a formal and declarative account of derived results that can include ellipses-style notation. The main application is to develop a graph-based language for reasoning about quantum computation: Quantomatic.

Posted by: John Baez on June 25, 2012 5:22 PM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

Thanks for reminding me of this! I tried it a while ago and couldn’t get it to compile, then forgot about it. But you prompted me to try a bit harder now, and it seems to be working. I haven’t figured out how to use it yet (there seems to be very little user documentation), but it certainly sounds promising!

Posted by: Mike Shulman on June 27, 2012 4:32 AM | Permalink | Reply to this

### Re: The Gamification of Higher Category Theory

Edward Z. Yang recently created an interactive tutorial of the sequent calculus and has a post on his thoughts on gamifying textbooks at his blog: http://blog.ezyang.com/2012/05/thoughts-on-gamifying-textbooks/

Posted by: sc on June 28, 2012 4:33 PM | Permalink | Reply to this

Post a New Comment