Better Judgement
In which I first grapple with existential crises, and then argue that hope springs eternal.
I have been following the AI news lately with a constant state of low-grade, stomach-rumbling dread. The most recent trigger is the spate of breakthrough results in mathematics solved via modern LLMs, but the dread has been accumulating for a while.
Among the many hats I wear, two of them are (1) theory researcher and (2) academic who publishes papers in AI venues. Both hats (in a manner of speaking) are violently on fire.
Let’s start with the first crisis. I spent much of the 2010s learning how to prove theorems, and then teaching my PhD students how to do the same. This is the core craft of both mathematics and theoretical computer science. But theorem proving is being automated at a pace that I am having difficulty grasping.
As part of DARPA’s expMath program, in April a bunch of NYU colleagues and I built Lea, a deliberately minimal Lean 4 theorem-proving agent. I will have much more to publicly share very soon, but within a span of 2-3 months, Lea — powered by the latest GPT/Claude models — has been able to prove multiple open problems in both math and TCS. Not only that, but Lea also autonomously formalizes these results, end-to-end, in Lean with fairly minimal involvement on my part. It appears that I am, rather literally, automating my own job. Voluntarily! In two years, 100% of math/TCS results will be AI-assisted or AI-generated. What then?
Now to the second crisis. For the last 15 years, I’ve been actively involved in peer review of publications. Anyone could submit a paper, even anonymously, to a conference or journal. A team of reviewers, editors, ACs, and program chairs would voluntarily shepherd each paper through a review process. Sometimes this gave useful feedback to the author to make the paper better, sometimes not. It was noisy and messy and unfair and people used to complain all the time. But that was the system, it worked, people participated in it, and papers which successfully passed peer review served as valuable chips for getting jobs, tenure, promotions, and bonuses.
There is no way in holy heaven that this current system survives two more years. Generating a full-length paper is now trivial. Just ask Claude or GPT nicely, and it can one-shot a thousand ICLR papers within a few hours. A fraction of these can even be “real”, in the sense that they contain meaningful new science. The problem is with the other fraction: perfectly formatted and clear, plausible-sounding, in-depth results, yet wrong in very subtle and hard-to-detect ways. The referee pool was barely coping before; how will they cope now?
But it struck me recently: these two crises are two sides of the same coin.
For all of scientific history, generating an idea was the expensive part; verifying it was (typically) cheaper. Proving a theorem was hard, confirming that a theorem was correct was (typically) easy. But AI has flipped that equation upside down. Proposing high quality ideas is now nearly free using the latest frontier models. So the bottleneck — the scarce resource, the rate-limiting step — for technological progress is the judge that verifies these ideas. Our scientific commons will very quickly be only as good as the filters that we build to separate out wheat from chaff.
If this thesis is true, then it has important consequences for theoretical research (math and TCS in particular), the business of academia, and the means in which we create and disseminate new results.
While all this sounds thoroughly depressing, let me now explain why I am actually more excited than scared.
In 1976, Appel and Haken proved the Four-Color Theorem. They did so by having a computer grind through an unavoidable set of 1,834 reducible configurations. This took some 1,200 hours of machine time (Ed note: in 2026 units, less than a second on a regular Macbook Pro). The mathematical community refused to accept this result: was it even a proof if no human could do it on their own? De Millo, Lipton, and Perlis wrote a famous 1979 position paper arguing that machine verification would never play a role in CS the way proofs do in mathematics, because proofs are social processes.
Fifty years later, how the tables turn! The results we now trust the most are the ones which have been formally verified to be true. My colleague and friend Anirudh Sivaraman recently wanted help with a half-complete proof; Fable closed it for him, but he was only convinced of its correctness after Lea mapped it out formally in Lean.
There are deeper advantages. A verifier fundamentally changes what you can ask for from an AI model. If verification is cheap, then the proposer can take enormous risks. This is complementary to Anthropic’s or OpenAI’s business: every stronger base model can only make this approach better, since this means that the space of accessible ideas can be expanded. This, I suspect, is why Silicon Valley has massively invested in rising startups like Harmonic, Axiom, and Math Inc.
But: it is useful to observe that some parts do not get automated. A Lean proof is only as meaningful as its formalization. Deciding whether a formal statement captures what you meant remains human. The craft of theoretical CS and of academic research will evolve: from proving theorems to evaluating how meaningful they are; from writing referee reports to building referees. Taste, wisdom, experience, and judgment: each of these appreciate, not depreciate, in value.
So: my job as a prover of theorems is being automated. My other job as a referee of papers is turned upside down. The new frontier is not about building better idea generators; it is time to concede that the frontier labs have won that race. It is time that we start building better judges.
I’ll end with a hot take: the best place to start is not mathematics at all, but with a small piece of silicon that you can hold in your hand. More on that in coming posts.