Beyond proofs: a 'conceptual track' for what human theorists still do

Three theoretical computer scientists are asking STOC, FOCS, and SODA, the field's three flagship conferences, to formally recognize a question the discipline has so far left informal: if an AI can grind out the proof in an afternoon, what is the human theorist actually contributing? Their answer, published Saturday on Scott Aaronson's Shtetl-Optimized blog as a guest post by Pravesh Kothari at Princeton, Raghu Meka at UCLA, and Prasad Raghavendra at UC Berkeley, is a "conceptual track," a separate conference lane for the work of defining problems, naming concepts, and building frameworks that an automated prover cannot replace.

Imagine a near-future in which AI theorem provers, a distinct category of AI tool designed to produce formal mathematical proofs rather than chat, can prove well-specified claims, including long-open ones, in hours and at nominal consumer cost. The hypothetical is the engine of the essay. If that future arrives, the work of mathematics stops being the bottleneck; the deciding what to prove and why does not. That is the labor a conceptual track would formalize.

The proposed track has five moving parts. It would sit alongside the existing proof-based program at STOC, FOCS, and SODA rather than replace it. Papers would be capped at under 10 pages, judged exclusively on conceptual merit, and explicitly agnostic to whether the underlying theorem is hard. Most consequentially, the paper "need not contain the proofs of the theorems." Instead, the authors would supply a Lean certificate, a machine-checkable record of a formal proof verified by the Lean proof assistant, as a supplement. The current calls for papers do not allow that shortcut. The STOC 2026 Call for Papers requires "proofs … that can enable the main mathematical claims of the paper to be fully verified" inside the first 12 pages. The FOCS 2026 Call for Papers requires the same within its first 10 pages and adds an explicit policy restricting authorship to humans and demanding disclosure of substantive generative-AI use. The FOCS policy is adjacent to the conceptual-track idea, but a different lever.

The authors use two counterfactual examples to argue that the conceptual layer survives even when the proof is automated. NP-completeness, they note, would remain the field's crown jewel even if a magic oracle collapsed P versus NP overnight, because the value is in the framework, not the proof. Polymorphisms, the mappings between the structure of constraint-satisfaction problems, would still be why 3-SAT is NP-complete while 2-SAT is in P. The work that survives the automation is the naming, the framing, and the choice of which object to study.

The human cost of the upheaval, including what happens to graduate admissions, hiring, and tenure lines, is, in their words, a more important question the proposal deliberately does not address. They set aside the Millennium Prize controversies and the motivations of AI companies, and they concede that current AI systems still fail in ways their hypothetical ignores. Aaronson's foreword adds a second disclaimer: the three authors speak for themselves, not for the theory community, and the post is meant as "an excellent starting point for further discussion."

STOC 2026, the 58th ACM Symposium on Theory of Computing, has already run in Salt Lake City from June 22 to 26. FOCS 2026, the 67th Annual Symposium on Foundations of Computer Science, scheduled for New York November 8 to 11, passed its April 1 submission deadline and July 3 notification date months ago. Any new track that emerges from this conversation will, at earliest, shape STOC 2027 and FOCS 2027, whose organizing committees form over the coming year. The proposal is being seeded now, while the rules for those 2027 calls are still malleable.

The next test is narrow: whether the 2027 program committees for STOC and FOCS adopt the conceptual-track language in their calls, and whether SODA, the third venue named, follows.