On the day a proof outran its readers

Copyright: Sanjay Basu

The proof nobody read

On a Friday afternoon last November, an autonomous system called Aristotle was handed a problem Paul Erdős had posed roughly thirty years earlier. Six hours later it produced a proof. The proof was a long file of Lean 4 code, full of lemmas that no human had read. Verification took about a minute.

Somewhere in the middle of those six hours, Aristotle did something the working mathematics community had quietly failed to do for a generation. It noticed that the problem, as published in the official list of Erdős open problems, had a small gap in its statement. A hypothesis was missing. With the hypothesis added back in, the question reduced cleanly to a corollary of Brown’s criterion, and Aristotle proved that version. The hard version, the one Erdős presumably meant to ask, is still open.

You can read the Lean file. It is on GitHub. I have looked at it. I cannot really tell you what it says. The kernel of Lean, the small piece of trusted code that does the actual checking, is small enough to audit by hand, and a thousand researchers have done that audit over the last fifteen years. So we know, with the kind of certainty that has nothing to do with reading, that the file proves what it claims to prove. We trust the proof the way we trust a calculator with a thirty-digit expression. Not by following along.

In classical mathematics, a proof was the thing you understood your way into. The journey was the point, the destination came along for the ride. Aristotle inverts that. The destination is unambiguous and the journey is, for almost everybody on Earth, a closed book.

Sit with that for a second.

This essay is about a strange convergence happening this spring. Four fields that do not usually talk to each other (math, AI, philosophy, physics) have all walked into the same room from different doors. They will keep arriving over the next several weeks. In conference rooms in Munich and Porto. In arXiv preprints. In a Quanta cover story. In a Lean file on GitHub. The question, roughly, is what we mean when we say we know something nobody can grasp.

I want to write about it before the dust settles. The dust is not settling.

What if the safe were locked with an undecidable question

The graduate student who turned Gödel into a lock

Zero-knowledge proofs are old furniture in cryptography. The idea, sketched by Goldwasser, Micali and Rackoff in the mid-1980s, is that you can convince me a statement is true without telling me why. I leave the conversation persuaded and ignorant. For about four decades this has been useful for everything from anonymous credentials to private blockchain transactions to certifying that a particular machine-learning model was run on a particular dataset.

The catch is an old impossibility result by Goldreich and Oren. You cannot have a zero-knowledge proof that is also non-interactive, setup-free, and perfectly sound, all at once. Pick two. Cryptographers have lived inside that triangle ever since, trading a setup phase for some interaction, or trading perfect soundness for the computational kind.

Rahul Ilango, a graduate student at MIT, has now found a way to slip out of the triangle without breaking it.

The construction is hard to convey without slides, but here is the punch line. Ilango builds a proof system whose simulator, the imaginary entity whose existence is what makes the protocol “zero-knowledge”, may or may not actually exist. The catch is that ZFC, the axiom system most of modern mathematics rests on, cannot prove that it doesn’t. The simulator is Schrödinger’s witness. For any honest line of reasoning, it might as well be there. And that, as it happens, is enough.

Gödel’s 1931 paper is now load-bearing infrastructure for a cryptographic primitive. Incompleteness as a feature.

Ilango calls the resulting system “effectively zero-knowledge.” The IAS write-up uses the phrase. Scientific American picked it up. The preprint sits on the IACR ePrint archive as 2025/1296. Quanta covered the result on May 11 under the headline How Unknowable Math Can Help Hide Secrets, which is one of the better Quanta headlines of the year.

Think about the safe metaphor for a moment. A traditional cryptographic safe is locked by a hard problem. Factoring large integers. Finding short vectors in lattices. Things we believe a computer would take a very long time to solve. An attacker who throws enough silicon at it eventually wins. Ilango’s safe is locked by a different kind of barrier. The tumblers are statements that may or may not be provable in ZFC. There is no amount of compute that gets you through. The wall is foundational, not computational.

In Aristotle’s case, the proof exists and almost nobody understands it. In Ilango’s case, an object necessary for the security exists in a sense that mathematics itself cannot fully resolve, and that is exactly the source of the security. Two different kinds of incomprehension. Both doing work. Both load-bearing.

I want to call this unprecedented but it isn’t, quite. We will get to physics in a minute.

The bottleneck moves up the stack

Vanilla extract, not the cake

Terence Tao spent the back half of last year and the first half of this one writing about what is happening to his profession. He is not panicking. He is also not selling anything. He is doing the thing he is famous for, which is sitting with a problem for long enough that the right framing falls out.

In March he and Tanya Klowden uploaded Mathematical methods and human thought in the age of AI to arXiv, a piece commissioned for the Blackwell Companion to the Philosophy of Mathematics. The fact that there is a Blackwell Companion to the Philosophy of Mathematics, and that this question now belongs in it, is by itself a small data point about where we are.

The Nature interview a few weeks later was titled The job description is changing. Tao’s actual phrasing in the conversation is more interesting than the headline. He now uses AI to search the literature, to draft figures, to write code, to run calculations, and (this is the part that matters) to help him decide which of several possible approaches is worth chasing at all. The bottleneck has moved. It is no longer about doing the work. It is about choosing which work to do.

His best line is from a blog post a couple of days after the arXiv upload. AI in mathematical research, he says, is like vanilla extract. A bit of it makes everything taste better. Too much ruins the dish. Nobody should drink it straight.

I have been thinking about that line for two months. It captures something the cheerleader-versus-doomer binary keeps missing. The cheerleaders want to drink the bottle. The doomers want it confiscated. The working mathematician adds a quarter teaspoon and gets back to the cake.

There is a quieter literature running alongside Tao’s. The mechanistic interpretability papers. A May arXiv preprint on sparse attention post-training showed that you can prune attention edges in a trained model by something like a hundred times and still recover a circuit small enough to actually look at. The other one, on sparse dictionary learning, came out the same month and offered a unified theory of why these decompositions work, including a piecewise biconvex analysis of where the optimisation can get stuck. I am simplifying. The point is that there is now a research programme whose goal is to read the network back. To take outputs we have already accepted into infrastructure and produce comprehension after the fact.

That is the opposite arrow from the Aristotle story. Aristotle generates verified outputs no human grasps. Interpretability tries to grasp outputs we have already learned to trust. Two sides of the same coin. Neither one is going away.

The job description that is changing is not “do mathematics” turning into “do nothing.” It is “do mathematics step by step” turning into “survey, choose, verify, integrate.” A cartographer’s job, not a hiker’s. The drone covers a thousand square miles a day. The cartographer still decides which features matter.

Physicists invented this club. They will let us in.

We have been doing this since 1925

Here is the slightly contrarian turn.

The comprehension gap is not new. Physics has been living inside it for a century and has developed something close to a healthy relationship with it. The rest of us are joining a club with a long tradition.

Quantum mechanics is the obvious case. We have an operationally flawless theory. The transistors in the device you are reading this on were designed using its consequences. MRI scanners, atomic clocks, the laser in the DVD player you used to own. Engineering by the bucketful. And the “what is the wavefunction really” question has been openly contested since the Solvay Conference in 1927, and shows no sign of being settled by 2027. Pick your interpretation. Many worlds. Pilot waves. QBism. Spontaneous collapse. Working physicists, by and large, do not pick. They calculate.

I went looking through this month’s physics news for a fresh example and there were embarrassingly many. Quanta covered a group that produced “driven” magnetic quantum states by hitting materials with carefully timed pulses, generating exotic phases of matter that are surprisingly robust against the kinds of errors that plague quantum computers. The phases exist. The math describes them. Whether anybody can draw a picture of them is a different question.

In neutrino physics, recent results have all but ruled out the simplest sterile-neutrino hypothesis, the one that would have neatly explained the LSND anomaly, the MiniBooNE excess, the reactor flux deficit, the gallium anomaly. The anomalies are still there. The clean story is gone. The community is now in the slightly awkward position of knowing the data are real and not knowing what story to tell about them. I want to insist this is a normal scientific situation. It only feels uncomfortable because we have romanticised the moments when the story snaps into place.

A paper that picked up an honorable mention in the 2026 Gravity Research Foundation essay competition proposes that quantum dynamics is itself governed by something called “infrared gravitational configurations” with a Berry-connection structure characterising “infrared-dressed gravitational states.” I read that sentence three times. I am pretty sure I understand the formalism. I have no picture in my head for what it describes. This is fine. This is how physics has been for a century. Formalism is what you have when pictures fail.

Pilots have an instrument-flying mode. You lose visual contact with the world outside the cockpit and you trust the panel instead. Beginners crash because their inner ear screams at them and they listen. Experienced pilots fly the panel. Math and AI and bits of philosophy are about to learn the same skill.

Geist gets a peer reviewer

Hegel in the age of the autocomplete

The conference is Knowledge Without Comprehension? On Spirit after Hegel in the Age of AI, at the Munich School of Philosophy, May 21 through 23. It honours Slavoj Žižek. The framing question is the title of this essay, lifted intact, because I could not improve on it.

One paragraph of Hegel digression, because the conference earns it and I will not pretend a thousand-word section can do more. Geist, in Hegel, is the long historical process by which spirit comes to understand itself. The arc bends toward self-comprehension. Knowledge that is forever opaque to its knower is, on the Hegelian reading, a contradiction in terms, or at best an unfinished step toward a comprehension that will arrive eventually. A world that keeps producing more knowledge while never closing the gap between knowing and understanding is either Hegel’s nightmare or, depending on how you read the dialectic, its strangest fulfilment. I am not going to settle that here. The philosophers in Munich will not settle it either, but they will at least disagree in higher resolution.

A philosopher at Cambridge has been making a related argument about AI consciousness. The only honest position, he says, is agnosticism. We have outputs that are increasingly indistinguishable from those of conscious beings. We have no inner-story access. Forming emotional ties to such systems, he warns, could be “existentially toxic.” The phrase is overheated but the point underneath holds. It is the same epistemological shape as the math case. Behaviour we cannot explain, all the way down.

At Porto in early May, the 6th International Conference on Philosophy of Mind made AI its centre of gravity. Chapman ran an AI Epistemology Workshop in February. The infrastructure for thinking about this is being built in real time, by people who are, on the whole, taking it seriously rather than well-actually-ing it.

The everyday version of this question is closer to home than the Hegel framing suggests. You are already using systems that know more than they can explain to you. The recommender that surfaced this article. The imaging AI that may have read your last scan. The search engine that ranks your results. The autocomplete in your IDE. Knowledge without comprehension is not arriving. It arrived. We have been pretending it hasn’t for the better part of a decade.

The question is what habits we develop next.

When literacy spread in early modern Europe, a generation invented the footnote. A small piece of cultural machinery for tracing a claim back to a source. We are due for the next such invention. Something between a footnote and a Lean proof. Between a citation and a confidence interval. Between “I know” and “the machine says, and the machine has been right ninety-seven percent of the time on problems shaped like this one.”

We do not have a word for that yet. Munich will not give us one. But that is the shape of the thing we need.

On luxuries we mistook for guarantees

What comprehension was always for

Comprehension was not a guarantee. It was a luxury, available in the regimes where our intuitions happened to map onto reality. Newtonian mechanics fit our muscles, more or less. Throwing a ball. Swinging a hammer. Watching a planet wobble. The math caught the picture, the picture caught the math. For about three centuries that coincidence was so reliable we mistook it for the nature of knowledge itself.

QED never fit our muscles. General relativity didn’t. Deep learning doesn’t. Most of the universe was always going to require instruments. Comprehension is what happens when the instruments are simple enough that we can pretend they aren’t there.

Comprehension is what happens when the instruments are simple enough that we can pretend they aren’t there.

One worry I want to flag before closing. There is a difference between knowledge without comprehension and belief without comprehension. The Lean file proving Erdős #124b is the first kind. The chatbot that confidently cites a paper that doesn’t exist is the second. A quantum state we cannot picture but can prepare is the first. A model that hallucinates a recommended drug interaction is the second. They look superficially alike, an output you cannot verify by inspection, and they are not the same thing at all. The first is a frontier. The second is a hazard. Distinguishing them is going to be the central literacy of the next decade. I do not think we are very good at it yet.

The same week the Aristotle story made the rounds, Ilango showed that even the things we cannot know can be turned into tools. That is the move. Not “comprehend everything,” which was always a fantasy, but “build the right relationships with the things you cannot.”

The proof exists. The simulator may or may not. The conference is in Munich.

Sources

Mathematics and cryptography

Rahul Ilango, Gödel in Cryptography: Effectively Zero-Knowledge Proofs for NP with No Interaction, No Setup, and Perfect Soundness, IACR ePrint 2025/1296. https://eprint.iacr.org/2025/1296

Quanta, How Unknowable Math Can Help Hide Secrets, May 11 2026. https://www.quantamagazine.org/how-unknowable-math-can-help-hide-secrets-20260511/

Institute for Advanced Study, How Effectively Zero-Knowledge Proofs Could Transform Cryptography. https://www.ias.edu/news/how-effectively-zero-knowledge-proofs-could-transform-cryptography

MathArena, ArXivLean benchmark, March 2026 release. https://matharena.ai/arxivlean/

AI for mathematics

Harmonic Aristotle and the Erdős #124 announcement, Hacker News thread. https://news.ycombinator.com/item?id=46094037

Sebastien Bubeck on the easy versus hard distinction in Erdős #124. https://x.com/SebastienBubeck/status/1995159227170701753

Lean formalisation of Erdős #124b, plby/lean-proofs on GitHub. https://github.com/plby/lean-proofs/blob/main/src/v4.24.0/ErdosProblems/Erdos124b.lean

Tao and Klowden, Mathematical methods and human thought in the age of AI, arXiv 2603.26524. https://terrytao.wordpress.com/2026/03/29/mathematical-methods-and-human-thought-in-the-age-of-ai/

Nature, The job description is changing: mathematician Terence Tao on the rise of AI. https://www.nature.com/articles/d41586-026-01246-9

Tao on AI as vanilla extract, Adafruit blog summary. https://blog.adafruit.com/2026/03/30/terence-tao-on-ai-and-mathematical-thought-vanilla-extract-not-the-cake/

Sparse Attention Post-Training for Mechanistic Interpretability, arXiv 2512.05865. https://arxiv.org/abs/2512.05865

A Unified Theory of Sparse Dictionary Learning in Mechanistic Interpretability, arXiv 2512.05534. https://arxiv.org/abs/2512.05534

Physics

ScienceDaily, Scientists just created exotic new forms of matter that shouldn’t exist, May 4 2026. https://www.sciencedaily.com/releases/2026/05/260504154014.htm

Quanta Magazine physics section, early May 2026. https://www.quantamagazine.org/physics/

Quest for Quantum Gravity, arXiv 2602.11806, 2026 Gravity Research Foundation honourable mention. https://arxiv.org/html/2602.11806v1

Philosophy

Knowledge Without Comprehension? On Spirit after Hegel in the Age of AI, Munich School of Philosophy, May 21 to 23 2026. https://philevents.org/event/show/146149

hegelpd notice for the Munich event. https://www.hegelpd.it/event-knowledge-without-comprehension-on-spirit-after-hegel-in-the-age-of-ai-munich-21-23-may-2026/

6th International Conference on Philosophy of Mind: Artificial Intelligence, University of Porto, May 4 to 8 2026. https://philevents.org/event/show/143946

We may never be able to tell if AI becomes conscious, argues philosopher, University of Cambridge. https://www.cam.ac.uk/research/news/we-may-never-be-able-to-tell-if-ai-becomes-conscious-argues-philosopher

AI Epistemology Workshop, Chapman University, February 2026. https://www.chapman.edu/scst/conferences-and-events/conferences/ai-epistemology-workshop.aspx