Shut Up and Prove

TLDR; We are at an asteroid hitting the earth level of crisis of intellectual life.

My first love was the foundations of mathematics. Or maybe the second love; the first was quantum mechanics. But my first love where I had any kind of technical purchase on the domain of inquiry was the foundations of mathematics. In fact, I think I read a proof of Gödel’s theorem and tried to understand it, and perhaps even rework it, before I was truly fluent in much older kinds of mathematics, like the differential calculus.

So I went to study mathematics thinking I would go deep into the foundations. I don’t know if you’ve read Logicomix, the fantastic graphic novel about the crisis in the foundations of logic and mathematics in the early twentieth century, but those images of Bertrand Russell almost going mad because he couldn’t understand how one could guarantee certainty: those are the kind of intellectual feelings I mean.

From Logicomix

I was still a teenager then, so I’m sure my intuitions weren’t coded in these philosophically precise ways, but nevertheless, this idea that there is bedrock, that there is this most general science, has always been a pull for me. At that time the foundations of mathematics felt like the only thing worth doing. Not number theory, not the romantic idea of the Indian mathematician that Ramanujan represented, but rather a philosopher-mathematician that Bertrand Russell represented, and who probably went out of fashion in 1939. Russell did say:

The mathematicians do not read Plato, while those who read him know no mathematics, and regard his opinion upon this question as merely a curious aberration.

Anyway, I got to college thinking I would study the foundations of math. There were no classes on offer. I went to an engineering school where, first of all, there were no abstract math classes for the first two years, and secondly, my fellow students didn’t care about intellectual questions. They just wanted to solve problems, and perhaps fix things. Actually, at the IITs, nobody fixed anything. I think the idea of smarts was just to do well on exams.

So I spent several years as an undergraduate realizing that nobody, at least in the math circles I was in, cared about these foundational questions. They mostly didn’t care about intellectual questions. Sometimes they cared about scientific questions, but they most certainly didn’t see themselves as intellectuals.

Shut up and calculate.

Then I went to grad school, to a department that was famous for mathematical logic. And I quickly realized when I got there that mathematical logic was, at least at that time, seen as separate from the mainstream of mathematics. It was an island of its own in a much vaster sea, and “real mathematicians” didn’t care about foundational questions. Or maybe foundational questions were taken to be solved. Either way, the attitude was, “Shut up and prove.”

I tried shutting up and proving for a while, but my heart was never in purely technical questions. It’s never been in purely scientific questions either, if by science you mean empirical inquiry that is very closely tied to the data and doesn’t have conceptual or intellectual richness beyond what the experiment is going to tell you. It’s not surprising that I first got interested in quantum mechanics and then in the foundations of math, because those were both areas of inquiry that, in the first half of the twentieth century, led to massive conceptual leaps.

But by the time I came of age, these foundational questions were left by the wayside. Quantum computing and information brought them back into physics to some extent, but mathematics never had its come back to Jesus moment.

And so I left mathematics to study consciousness and cognitive science, because as it turned out, those were the disciplines where the conceptual questions were far more alive. If you’ve been reading my writing about unicellular cognition, we are at the cusp of a major conceptual revolution in our understanding of the mind. But we won’t go there today, for I want to talk about conceptual revolutions in the study of mathematics.

Fast forward a couple of decades. The “shut up and prove” model worked really well until about a week ago. Or maybe three months ago. If you’re reading this, you probably know the reason: AI. Of course.

Just a few hours before I’m wrote these words, OpenAI gave notice (there’s a lot of controversy behind it, but I won’t talk about that) that one of its teams has solved the Navier-Stokes conjecture, one of the open Millennium Problems. The solution, if shown to be correct, comes with a million-dollar prize. Not that OpenAI cares; a million dollars is a drop in their bucket. They probably spent more than a million dollars on tokens to prove the conjecture. Setting aside these commercial details, it looks like AI has finally solved, provably so, because I believe there is Lean code that guarantees the proof, a problem that the mathematical community would consider Fields Medal-worthy if it had been done by a human being. Built, of course, upon the work of many human beings who came before it, trained on their output, and perhaps, if the rumors are correct, not only trained on the output of past human beings but actually using the private chats of other mathematicians who are also using Claude, not ChatGPT.

But those are all details.

Yes, there’s the ethics of mathematics, who is supposed to get credit, did OpenAI steal data. All of these things are there. But I want to talk about the far more salient fact, which is that “Shut Up and Prove” is a failed strategy now. Because there’s something else which is not even going to want to speak, which doesn’t have the intellectual pretensions that you do, and which will prove a lot more a lot faster than you ever can.

In just the last two months, if you look at what Anthropic and Google and OpenAI have achieved, there is no doubt in my mind that at this time next year AI will have replaced a great deal of SHUP human mathematics. And whether or not there will be some human mathematicians left who are better, for some definition of ‘better’, the business of theorem proving is no longer the business of human beings. This is my assessment, but I am far from the only person thinking so.

Maybe some human beings will prove some theorems here and there. It’s not like chess, where you are competing with the machine on the same board with the same rules. Your rules might be a little bit different. But any time there is substantial progress, the AI companies are going to be listening to where the progress is being made, and they will scoop all of that up and make more progress than you will.

But who cares whether they do that or not?

The fact is that a certain model of doing mathematics, where proving five-star theorems gets you all the laurels, or even the more expansive version, where you do symbolic mapping of abstract structures into written symbols (printed or handwritten), and create proofs out of them, I feel like that business is no longer for humans.

Which means that you can’t shut up and prove anymore.

So besides whatever it is that mathematicians need to do to survive, this is, a serious intellectual crisis. A more serious intellectual crisis than the one that was almost driving Bertrand Russell to suicide. Because the kind of thing that mathematicians have done, not for a hundred years but for two thousand years, is now a dead end. At least for human beings.

No one could have predicted this foundational crisis. It’s not a crisis of a specific team or idea. It’s not like somebody has shown a contradiction at the root of mathematics. If that had happened, we would have gone about our professional lives and either repaired the contradiction or figured out that maybe math can live with contradictions. Those moves seem possible.

But the idea that machines are better than humans at rational inquiry grounded in symbolic reasoning that, for the most part, adheres to standards of proof and the law of non-contradiction: this means that the intellectual effort of formal inquiry, which mathematicians would have argued until a few weeks ago they represent in its purest form, is no longer a human inquiry. It’s not clear if AI inquires in any way that humans do. But humans cannot inquire by themselves anymore. Maybe humans working with machines will, but that’s a different topic.

What this brings me back to a fundamental philosophical question. I think that formal inquiry (and I don’t mean mathematical or logical inquiry alone) is a form of philosophizing, and one of the great achievements of humanity across cultures. If we stop doing formal inquiry, we are losing out on a pursuit that makes us who we are. Understanding the essence of form, and the various manifestations of form, gives a huge chunk of intellectual life its sense of purpose and meaning. Everything from religion to philosophy to art to metaphysics is permeated by this idea that formal reasoning, formal aesthetics, formal intuition, formal logic have deep insights into reality.

So what do we do when one of its major arteries is closed off for humans? I don’t know. But it’s a question that we have to ask, that shut up and prove relegated to the background. We have harmed ourselves by shunting intellectual questions about mathematics. In the absence of intellectual ferment, I see two pathways of resistance:

1. Various types of human-machine collaboration, with some things being proven really fast, creating open-source (or closed-source) platforms of Lean-guaranteed theorems that all other mathematicians and machines can build on. We have a lot of engineering work to do, for sure.

2. We also need to address questions about the political economy of mathematics: who gets access to these machines, do machine-generated proofs get prizes, and of course the big elephant in the room of capitalism capturing mathematics per se and turning it into an instrument of profit-making.

Or perhaps, a year from now, there will be a lot of mathematics left, not because the AI cannot do it, but because it’s no longer interesting to the AI companies. A couple of years ago they were all generating illustrations and videos; this year it is math, because that is great PR for them. Once math is done, they’ll move on to something else.

But be that as it may, political economy questions about who regulates AI in math, is it good to spend a trillion tokens to prove the Riemann hypothesis, what if we prove the Riemann hypothesis but it uses all the water in Texas, while these are questions worth asking, they are not the core intellectual questions. In fact, we don’t know yet how to even pose those questions. We don’t have the intellectual apparatus to directly address the future of formal inquiry that:

1. Isn’t reducing it to engineering, and

2. Isn’t explaining it away using socioeconomic models of explanation.

We need to explain formal inquiry in ways that are intrinsic to formal inquiry itself. Mathematics is a core human pursuit, and by extension, so are the other sciences. While we should obviously pay attention to how incentives for today’s mathematical inquiry are changing, we should not lose sight of the larger challenge to intellectual inquiry as a whole.

More soon.