← back

The fall of the theorem economy

David Bessis · Blog · July 20, 2026

This is one of the best things I’ve read in a while, between both writing style and actual substance. As such, summarizing this work doesn’t do it justice at all. I highly, highly recommend just reading the original blog if you’re reading this.

Miscellaneous, Unorganized Notes

As someone who considers themselves OK but still pretty mid at math, this section felt comforting to read:

Official math manifests itself as a formal deduction system where you start from axioms and mechanically derive theorems. This is a nerd’s paradise, a world where truth takes binary values, reasoning is either valid or invalid, and there is technically no room for bullshit.

Secret math is the human part of the story—why official math was invented, how we can successfully interact with it, its effects on our brains, and the bizarre mental techniques through which mathematicians continuously expand its territory.

Secret math never made it to the curriculum, because it lacks the defining qualities of official math, and also because it feels peripheral. Official math is cold, hard, logical, objective, and it is rumored to be the language of the universe. Secret math is soft, fuzzy, subjective and, by contrast, it looks like cheap pedagogical backstory.

• An overarching theme is that math, at its core, is human. This is not obvious imo. One can view the field’s goal as “proving every theorem,” combinatorially searching every way to combine existing theorems/lemmas/axioms, but the real value in math comes from creating important concepts for humanity. Historically, theorems followed from the latter, which is why they could be treated as the same. AI makes this not the case anymore.
• I think Bessis’s “Caveat 2” is pretty nuanced, and I’m not sure I agree with all of it. The TLDR here is that math, being for humans, must be canonized. Thus, arbitrarily large/incoherent auto-formalization of proofs is sort of useless. Quote from Patrick Massot:

  I think the situation is pretty clear: AI companies, and especially Math Inc, will indeed thoroughly bomb this area to turn it into a giant radioactive wasteland that will never be able to sustain life again, so we will never get the benefits expected from formalization (improved understanding and accessibility). I strongly advise young people to contribute to less shiny projects that are less likely to be destroyed.

This entire read made affirmed my more recent thoughts about how the arts are the ultimate callings for humans. Or something like that.