Yesterday OpenAI put 372 mathematical results on GitHub. They came from an internal model, nearly all of them from a single prompt to a single agent, at roughly three hours of compute apiece. Many arrive with Lean formalizations, which means a software program has checked every step, which means the proofs are likely valid.
Some of them are certified true, and no human has yet understood why. That sentence couldn’t have been written two years ago, maybe not last year.
Mathematics has had unread proofs before, from things like the four-color theorem, to Hales on Kepler, or even, more prosaically, classification results too long for any one referee. But those were long in ways people had chosen and that other people could inspect piece by piece. That strategy was ours even when the case analysis wasn’t.
What’s on GitHub is different, proofs whose strategy belongs to no one, certified by a kernel that vouches for validity and says nothing about meaning.
We now know things that, so far, none of us knows.
My initial reaction to this, frankly, was that it made my skin crawl. I couldn’t imagine a thing more alien than proofs, discovered by a human creation, that humans don’t and maybe can’t understand.
But Freud has the better word for it than my “alien.” In “The Uncanny” (1919) he works through the German unheimlich, the unhomely or uncanny, and concludes that it names the class of frightening things that “leads back to what is known of old and long familiar.” The uncanny isn’t the alien. It’s the familiar returned in a shape we can’t place. The doll that’s nearly a child, the double, the house that’s ours but isn’t.
Among the results is a claimed proof of the Unique Games Conjecture, a problem the complexity theorist Dana Moshkovitz has worked toward for her whole career. Her real-time reaction, relayed by Scott Aaronson, is that the proof invents a new and bizarre code, built by a recursive construction and checked with a noise test, unlike either of the codes the field already knew. She called it “some alien craziness,” and added that there’s a lot for us to learn from the aliens.
The word is the natural one. It was mine, too, at first. But now I think that it’s only half right. If these were alien artifacts, they’d be strange and nothing more, since the existence of alien provers would eclipse anything they’d proved. These aren’t that.
Whether you like AI or hate it, there’s no disputing its most distinctive fact. A language model is made out of us. In this case, out of every proof, textbook, lecture note and late-night forum answer mathematicians have ever written, compressed and recombined. The results are in our notation, they cite our lemmas, they answer questions we asked, in a discipline that is about as distinctively human as anything we do. And they’re illegible to the people they came from.
The model is us and it isn’t and these proofs are the plainest evidence yet of both. The model is uncanny.
Freud tells a story about himself in a footnote to the same essay. Sitting alone in a train sleeping compartment, he saw an elderly man in a dressing gown come through the door, rose to set him right, and realized it was his own reflection in the door’s mirror. He remembered disliking the man. That is closer to what’s happening here than any story about first contact.
The intelligence we can’t follow isn’t arriving from outside. It’s our own, caught at an oblique angle of recline that strikes us as jarringly odd.
Mathematics is a social practice as much as a body of truths. A proof was the thing that moved understanding from one head to another, and correctness was partly a property of that transfer. A proof was the thing that forced others to assume something about the world even before understanding fully landed.
I’m reminded of Turing’s proof that the halting problem is undecidable, which is almost comically simple. A student can follow it in an afternoon. But following a proof and grasping its implications are different kinds of understanding and the implications aren’t in the proof.
What the halting result means for computation, for mathematics, for what any procedure can know, took decades to work out. The Unique Games proof turns this around. Complexity theorists spent twenty years working out what the conjecture would imply, a whole map of which problems can’t even be approximated efficiently, and now they have the implications in hand and a claimed proof that nobody yet understands.
Twenty-five Fields medalists have already warned that results produced at this scale could exhaust fertile ground rather than seed it, which is the practical worry.
The human existential one is plainer. We’ve built a way of being right that doesn’t pass through anyone’s understanding and we built it out of our understanding.
None of this would have surprised Freud. He ranked his own claim, self-aggrandizingly but not wrongly, beside Copernicus and Darwin as the third great blow to human self-regard: the ego “is not even master in its own house.” We have never been transparent to ourselves, not really. We could only behave as though we were, so long as what we made stayed small enough to survey.
The proofs are us and we remain as opaque to ourselves as we ever were and now to our works and pomps as well. Freud met the self-stranger in the mirror of a sleeping-car door. Yesterday we met ours on GitHub.