The fall of the theorem economy

From the article:

In my first Substack post, I (half-jokingly) declared that we had been wrong about mathematics for 2300 years, stuck in a false dilemma between formalism (“mathematics is a meaningless game of formal symbols”) and Platonism (“mathematics captures properties of actual entities living in the perfect world of ideas”).

My proposed conceptualist resolution is a rephrasing of Thurston’s view: mathematics does rely on a meaningless game of formal symbols, but we only play this game because we project meaning onto it.

[...]

This is how the system worked for millennia. Mathematicians created value by introducing new concepts, but the rule was that only theorems could put bread on the table. The deal was fine because the two aspects almost always walked hand in hand. David, the social parasite who claimed credit for the 𝐾⁡(𝜋,1) conjecture, was the same person as the David who crafted Definitions 2.4 and 9.3.

Solving a big conjecture was a cryptographic proof that you had come up with a genuine conceptual innovation.

I am using the past tense because this is no longer the case. There is a structural vulnerability in the honor code of mathematicians and AI has started exploiting it in a systematic manner.

[...]

The problem with unintelligible proofs goes way beyond correctness, and cannot be resolved by autoformalization alone: even if correct, unintelligible proofs aren’t accretive to the mathematical corpus.

[...]

Yes, I know, that sounds counterintuitive. This is why outsiders are likely to miss the nuance and label the pushback as Luddism.

A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs and abstractions, without which no autoformalization could take place. By contrast, Math Inc’s autoformalized proof of Viazovska’s results exposes no intelligible interface. Who in their right mind would merge a 200,000-line unaudited vibe-coded blob into the master branch of global human science?

[...]

This is what made the Mathlib community so angry. They had been working on a multiyear project to formalize Viazovska’s work. Math Inc jumped in on this collective effort, leveraged prior insights, then abruptly went silent, until they made their spectacular announcement.

Is this necessarily bad news? Now that the brute-force autoformalization is done, why can’t the Mathlib community refocus on the value-creating canonization?

Because of Hardy’s curse and the honor code of mathematicians. Math Inc captured the prize (“first formalization of a Fields-medal-level theorem”) and there is no social reward left for cleaning up after them. Hence this comment by Patrick Massot, a non-Luddite expert in formalized mathematics:

[...]

The likely outcome is that formalized mathematics will now develop in two separate layers, an intelligible layer embodied by Mathlib, and an unintelligible layer we might call Mathslop, a library of results that are known to be correct via proofs that no human has ever understood.

[...]

Why don’t we construct benchmarks that are fairer to humans? Because we can’t. Because the true value of mathematics, the collective and individual elevation of our worldviews, is ill-defined and intangible. This intangibility was the raison d’être of the honor code.

For millennia, we had agreed to only benchmark human intelligence on its problem-solving facet, as we had found that it was the best objective proxy. Theorem proving is so inordinately difficult for our cognition that the only progress path was through patient concept building and neuroplastic internalization of these new concepts.

Yet this was only ever a proxy. The thing we really care about is different in kind. Industrial robots are far stronger than humans, yet we still go to the gym. Blenders have been outchewing us for over a century, yet we still don’t eat exclusively through straws.

[...]

If theorem-proving remains their only official currency, all research mathematicians run the risk of becoming demonetized in the course of the next few years.

[...]

All the active mathematicians I have cited, from Tao to Avigad, from Litt to Kontorovich, are careful to note that there is something in mathematics that goes beyond theorem proving. Yet this is usually framed as a passing remark, not a major shift in the narrative.

Well, this is a major shift in the narrative, and the public will never take it seriously if it isn’t properly explained. Right now, it looks like an excuse.