Ilya Sergey, a programming-languages researcher at the National University of Singapore, says the step that used to consume 80 to 90 percent of a PL paper’s labor now takes him about four weeks, working alone. He describes the shift in a post on his own blog, Proofs and Intuitions, timed to a new paper he co-authored, accepted to OOPSLA’26, one of the field’s top peer-reviewed venues. The paper’s type system for Move, a Rust-style smart contract language, is not the interesting part. How it got built is.
Mechanizing a paper’s meta-theory, turning an informal soundness argument into a machine-checked proof, has historically been the part of PL research that ate a team’s time: months of labor building formal models and grinding through proof obligations by hand. Sergey did that work for a production-scale compiler rather than a toy example, using a frontier large language model inside the Lean proof assistant, and finished in four weeks. He first described the underlying method in a March 2026 post. This week’s post is about what happened after he started talking about it.
The community’s initial reaction was skepticism bordering on dismissal. Sergey says colleagues told him the proof “must not have been hard enough” or that the approach is not how PL theory should be done. He reads that response as revealing something about the field’s incentives rather than about his method: research has earned credibility partly by displaying visible human struggle, and once that struggle becomes optional, the credibility test has to move somewhere else.
He offers a second data point beyond his own paper. Martin Rinard, an MIT professor who had never used Lean, spent roughly a month formalizing an optimizing compiler in the same proof assistant, then wrote and submitted a paper on it. Sergey treats that as evidence the method generalizes past his own case, not an isolated result.
The aggregate numbers back the pattern up. POPL submissions came close to doubling over the year, climbing from roughly 350 to 600, and Sergey says most of the increase is competent research rather than AI-generated filler. His conclusion is that the field’s ambition should now rise to match: problems on the scale of CompCert, a fully verified C compiler, or the seL4 microkernel, both historically multi-year team efforts, sit within reach of one researcher with a good idea and a few free weeks. He says PL researchers “will have to become more ambitious” now that the old wrapper of manual labor is gone.
That argument treats a doubled submission count as proof the field will simply absorb the new supply through higher standards. It skips a step. POPL’s program committee still has to read all 600 submissions with the reviewing capacity it had when there were 350, and reviewing, unlike proof mechanization, is not the part that just got automated. Sergey’s own numbers describe a familiar tension: production got cheap, and the layer that decides which resulting artifacts deserve anyone’s attention did not.
AI Insiders covered a version of the same gap this week in enterprise agent adoption: an investor’s argument that companies buying agent capacity have bought the ability to produce output, not the still-unbuilt machinery to judge whether that output clears a genuinely high bar. Sergey’s field is living a research-specific version of that same shortage. Reviewers now face twice the submissions with the same eyes and the same hours, grading work that got easier to produce but no easier to evaluate.
The operational lesson travels past programming-language theory. A team deciding what to build next should stop asking whether it can produce a given artifact, since a frontier model paired with a formal or automated checker now answers that question for most well-specified problems. The harder question, worth answering before the four weeks start rather than after the paper is written, is who judges the result and against what standard. For any team using generative tooling to compress a formerly expensive production stage, the next ninety days should go toward building that judgment layer, not just running the new production capacity at full speed.
Ilya Sergey published this essay on his blog, Proofs and Intuitions, on August 14, 2026.
