On 13 September 2026, Pravesh K. Kothari, an associate professor of computer science at Princeton, posted a numbered note titled Some thoughts on AI and Theory. Theoretical computer science, he writes, has been organized around a few major open questions. Much of the work is problem-motivated: people invent methods in order to answer those questions. That work often produced theory, a general principle that unifies a class of theorems, but the theory-building still meant proving new, difficult theorems.
He is clear about the culture. Problem-solving was correlated with understanding, connections, and general theories, and the community, perhaps disproportionately, celebrated the solving. That was defensible. Progress on central technical questions usually tracked taste, creativity, persistence, and depth. The reward structure treated an important proof as evidence that someone had those harder-to-observe qualities.
The change he expects is that AI tools will soon prove many such theorems quickly. The cost of proofs for well-posed mathematical questions will likely fall. Scarce work then moves in two directions. Upstream: questions, models, theories, definitions, conjectures. Downstream: interpretation, synthesis, explanation, theory-building. Human understanding of the science still matters, he says, if humans are to stay meaningfully in charge of collective decisions. He says he will expand on that later.
The mechanism is in the sixth point. Finding a solution and understanding its significance used to be entangled, because finding a proof usually required discovering the right concepts along the way. A sharp drop in the time and effort to prove theorems could break that coupling. "We could end up with many more true statements and proofs without a commensurate increase in understanding." Converting an abundance of proofs into human understanding, he writes, may become one of the central challenges of the field.
From that he expects the high-level goals of theoretical computer scientists to change. Powerful theorem provers might help construct new theories and explore new models faster, and expand the domains those theories cover. In that sense the space for theoretical work may expand rather than contract. He closes on the human cost of the disruption, the range of reactions in mathematics and theory, and notes that work on the scientific and institutional questions is already underway, including at the Simons Institute.
The post is a set of expectations, not a measurement. It does not name a system that already proves the open questions, and it does not show that understanding has already fallen behind proof volume.
Editorial
The load-bearing claim is the coupling, not the timeline. A proof used to be expensive enough that you could not finish it without inventing the concepts that made it make sense. That is why a proof could stand in for taste. Once the proof of a stated lemma is cheap, the proxy dies, and the field has to score the question and the explanation directly.
"Well-posed" is doing the work. A tool that can grind a lemma someone already wrote down is not a tool that can decide which lemma is worth writing down. The famous open questions in the field are not waiting on cheaper algebra. If scarce work really moves upstream, the bottleneck is which problem to chase, and there is still no grader for that.
The expansion story in his seventh point does not follow from the sixth. More true statements can fill journals without filling understanding. Provers might help people try more models. They might also bury the few connections that matter under a pile of verified trivia. He does not settle which. The honest remainder is the conversion problem he named, and the institutional one he only points at: if proof is no longer evidence of the qualities the field wanted, something else has to be.