Raw capture — raw/canonization-and-the-overhang.md
url: https://laughingmeme.org/2026/06/30/canonization-and-the-overhang.html title: Canonization and the Overhang author: Kellan Elliott-McCrea date_fetched: 2026-07-08 date_published: 2026-06-30
Author: Kellan Elliott-McCrea Date: June 30, 2026
The article responds to David Bessis's piece "The fall of the theorem economy," which the author finds compelling despite not being fully qualified to assess all its claims. Bessis identifies trends familiar to engineering leaders and offers two useful terms.
Bessis argues that mathematics has publicly rewarded theorem-proving as high-status work while undervaluing creativity, community, clarity, and teaching. Critical work occurred as an "unacknowledged byproduct of the system of human production," but with LLM-powered theorem provers, that proving can happen "in the absence of those critical side effects."
The author draws parallels to software, asking how we should value code that merely passes tests versus code "socially constructed in a way that leaves the team prepared to operate on it." Similarly, what's the value of "200k lines of unintelligible Lean autoformalization?"
Canonization is borrowed from Alex Kontorovich, who describes it as "taking a local, one-off formalization and turning it into library mathematics: general, reusable, coherent, efficient, and compatible." This is the work of turning something that works into something the future can build on.
Bessis claims the "only true value of proving a theorem is for the practitioners that follow." But in software, the author notes, we have the inverse: disposable production code is a key learning tool — the MVP concept. Everyone benefits from canonized code: stable abstractions, reliable systems, encoded best practices. The current phenomenon of "vibe coded" solutions feeling more reliable than established ones reflects a lack of canonization. The author references their earlier piece distinguishing "getting lines of code into a text file" from canonization, calling it "the photo negative of technical debt." Features that resist change and drain morale indicate an absence of effective canonization (or evidence of bad canonization).
We're in a golden age of disposable single-use software that reads as "bad" by older aesthetic standards. Canonization makes explicit what those standards were doing implicitly — it separates "work that does today's task and work that is accretive."
The Overhang is Bessis's term for "the unrealized capital gains of past (mathematical) creativity" — latent value from connecting existing work. It's "a dividend of canonization." Mathematician X states a problem, Y crafts a concept, Z notices B solves A and captures the social reward, but in doing so introduces new concepts, "reinjecting latent value into the Overhang."
LLMs, capable of memorizing entire corpora and pattern-matching, are well-suited for searching the Overhang in ways distinct from human cognition — humans rely on intuitive leaps from limited reading and interpersonal interaction.
Software has its own Overhang: open source, decades of canonized work in public repos, Stack Overflow, blogs. This allows discovering things that wouldn't emerge from human brains alone. The author references Highlander II as a long-ago dream of searching such a space.
The author dislikes Bessis's term "intuition-maxxers" but is excited about people "seeing further than anyone before, standing on the shoulders of giant machines."
A warning follows: if we value only theorem-proving (coding) and not canonizing nor training new practitioners, the "Cognitive Surplus" becomes "Cognitive Seed Corn" — the Overhang will grow poor as a search space. Reviewing grows more fatiguing and unrewarded; cleanup earns no status. The author cites Tanya's work on "glue work."
"Generation easy. Canonization hard." Running code and presumably autoformalization have value. But intuition and "the social production of knowledge are the seed corn." The task is to reimagine how teams work and what receives status, so "our practices don't leave our people or the Overhang depleted."