Zelda Got it Right#

Author: Steve Kieffer

There is a category of very popular and fun video games, in which your character is on a grand quest, filled with side-quests and incremental achievements. Maybe the grand quest is to defeat the evil wizard, and save the kingdom. But first you have to clear nine dungeons. In order to reach the first dungeon, you have to get across the river. So you’ll need a raft. To get a raft you have to gather sticks and bring them to the shop where they make rafts. And, just like that, you find yourself excited about gathering sticks! Who would have thought?

When you play these video games, you’re excited because you have a purpose in mind. You think to yourself, once I get those sticks, I can get that raft made, and then I can get across the river and clear the first dungeon. Then it’s off to the second dungeon. And when I’ve cleared all nine, I can go to the final boss and win the game!

What I propose is that we structure the quest to understand a vast mathematical proof in the same way. (I am not the first to compare proof writing to video game achievements [Buzzard].) Take Fermat’s Last Theorem, for example. The grand quest can be stated in a few words. (Let me apologize in advance if I get any of the details wrong.) We can say to the student: Here’s the Frey curve. It has three parameters, \(a\), \(b\), and \(n\). If those parameters satisfied a Fermat equation \(a^n + b^n = c^n\) for some integer \(c\), and \(n\) an odd prime, then this curve would not be modular. Understanding this much is Dungeon 1. Dungeon 2 is: the Frey curve is semistable. Then we move to Part II of the game, where proving that all semistable elliptic curves are modular spans several more dungeons.

With this “overworld map” in view, we feel motivated to get into the side-quests and incremental achievements. We’re now really excited to understand the definition of semistable, because it has just become our “raft.” We already have a purpose in mind for it, and can hardly wait to use it. I think this kind of “extension of motivation” might have been partly what Tim Gowers had in mind, when he wrote

“Many textbooks begin with definitions that justify themselves later by leading to interesting results: this would be forbidden in the kind of textbook I have in mind. Instead, every definition should be presented as arising naturally in the search for the solution of some problem.” [Gowers]

The hierarchy of goals thus extends accessibility and motivation from the theorem statement itself, all the way down to the most minute of tasks. The theorem statement is immediately accessible. Anyone can read it, understand it, and feel motivated to prove it. That motivation then extends to the proof’s top-level goals, and then onward to the next level of subgoals, and so forth.

The trick for us as teachers, if we really want to make “Math: The Video Game” is to keep this hierarchical structure going all the way down to the ground level. We have to take Dungeon 1 and break it down into three or four steps, each easily stated, though not necessarily easy. Each new statement makes a new goal. Now we can dig down into the next level, and find the next three goals that lie below that one, and so on. Eventually, after digging long enough, the student reaches a goal that is immediately achievable. And that goal then becomes the first step of a long journey.

Proofscape provides a way to manage the “top-down” study of mathematical proofs in precisely this way.

In Proofscape, expansions provide for the hierarchical structure. We also have “overworld maps”, which we call theory maps. These can be generated in the PISE software, and they show either all the theorems a given proof relies on (a “lower” theory map), or all the proofs that rely on a given theorem (an “upper” theory map). There is even the equivalent of an “item screen” (we call these study pages) where the student can see a summary of all the goals in a given study, including those they have achieved so far, and those they have yet to achieve.



Buzzard, Kevin. “Proving theorems with computers.” Notices of the AMS 67.11 (2020): 1791-1799.


Gowers, W. Rough Structure and Classification. Geometric and Functional Analysis, Special Volume – GAFA2000, 1-39. 2000.