An essay by Brendan Caldwell made the rounds recently arguing against video games like Vampire Survivors that automate a key verb in their genre (in this case shooting) without changing what the player sees (a vampire hunter shooting monsters). Reading it, I couldn’t help but see parallels to the transformation currently underway in research mathematics. How different is watching an LLM connect lemmas to each other while you vaguely steer it to watching a pixelated vampire hunter throw axes while you…vaguely steer it? Vampire Survivors moves the player’s agency away from aiming and firing onscreen projectiles to picking a direction to walk the onscreen character and to choosing upgrades like stronger weapons or more health. In Brendan’s words “Self-playing games take microdecisions away from you in favour of macrodecisions.” If you play games because you enjoy those microdecisions then this is going to be really frustrating.
However, macrodecisions can be really fun. In 2013 a free game called Cookie Clicker went viral and, though it borrowed heavily from a few earlier games, is generally credited with creating the idle game genre. In an idle game the player is expected to make only macrodecisions. The core of an idle game is a currency (cookies, say) that accumulates automatically over time and that the player can spend on “upgrades” to increase the rate at which the currency accumulates. Choose the right upgrades and you can progress through the game relatively quickly, seeing more content and achieving higher quantities of the currency. Choose the wrong upgrades and you might remain stuck in one part of the game for hours or even days waiting to have enough cookies to move on.
In a typical video game, a player’s score or progress increases at a rate that depends on their skill (e.g., how well they shoot vampires). In an idle game, a player’s score increases automatically but the rate at which it increases is set by the player’s skill in choosing upgrades to manipulate that rate. In other words, idle games move the player’s input from the first derivative of the score to the second derivative. Vampire Survivors is, for Caldwell, an uncomfortable hybrid that teases control over the first derivative while really being about the second. The subjective experience of control at these two levels is very different and expecting one kind of game and getting the other is jarring.
This then brings us to mathematics. Today all of our mathematicians are trained to make progress directly. A more skillful mathematician can move faster on harder problems and so has a higher first derivative for mathematical progress. For a person who has honed their mathematical skill, watching LLMs make any contribution to the first derivative of mathematical progress at all is a serious change. In areas where that contribution has increased to the point that supervising LLMs is more efficient than doing mathematical work directly, there’s a widespread and very sympathetic view that this change kind of sucks. In particular, it sucks in exactly the way that expecting to shoot vampires and having the game do it for you sucks.
As Terrence Tao and collaborators have argued eloquently over the past several months, solving problems is not the point (or at least not the only point) of mathematics research as a human activity. Nevertheless, mathematical progress isn’t just for the benefit of mathematicians. Ben and I previously argued that we think AI is likely to be a great tool for applying new mathematics to scientific challenges. If AI can solve open mathematical problems, even if it does so in a “bad” way, and help us apply those solutions to scientific work the pressure to continue in this direction will likely prove irresistible. If this happens, w could see a bifurcation in mathematics between a body of knowledge that is understood and accepted by research mathematicians and a larger body of formally verified mathematical facts (and hopefully human-readable explanations of those facts) that can be applied to describe, predict, and control natural phenomena. In this hypothetical future, applied mathematics will incorporate results that pure mathematics does not, inverting their centuries-old relationship. Mathematicians may soon find themselves drowning in both useful but unfulfilling pseudomathematics1 and ennui.
In video games at least, it’s possible to have a great time making only macrodecisions. If LLMs start to make mathematical progress in the sciences feel more like “number go up,” making and enjoying those macrodecisions is going to matter more and more. Cookie Clicker’s official achievements cover 72 orders of magnitude of cookie production; how many orders of magnitude of mathematical progress for science are out there? Even considering the finiteness of natural phenomenon and of the human mind’s ability to understand them, there must surely be at least a few more orders. Could we get applied mathematics moving 10 times faster, 100?
If we can, the macrodecisions are going to be tricky. Any mathematical progress has both a magnitude and a direction. Just like in Vampire Survivors, choosing which direction to walk your automated monster slayer/theorem prover matters. I’d bet that there’s infinite (or effectively infinite) possible mathematical progress and only finite applied mathematical progress that are practically accessible to humans. If that’s the case, humanity could pour arbitrarily large amounts of money and compute into mathematics without getting any practical results to show for it. In that scenario, macrodecisions about what to work on and how to work on it will be all we have.
Despite the legitimate concerns of mathematicians, there are no humans better trained or better placed to make these macrodecisions. As a skilled shooter of pixelated vampires myself, I had an eye for which upgrades and strategies would work best in Vampire Survivors even though playing it felt completely different than playing any of its microdecision-based forebears. Once I let go of my expectations, I had a great time. And so I entreat the mathematical community: come be our yokefellows as we try to understand and shape the world. We could use orders of magnitude more applied math, even if its foundation is a mess by historical standards.
And, for every layer/derivative that AI automates, there will always be a layer above it where someone has to decide what’s best for humans. Otherwise, you get a paperclip maximizer which of course is the subject of an excellent idle game.
There isn’t yet a word for math that is formally verified, not digested but the mathematical community, and still applied to natural phenomena. I’m sure this isn’t the best option and I’m open to suggestions.