Great essay, thanks for sharing.
When I was a software library developer, I came to resent application developers. I noticed a pattern. Libraries solved hard problems and did so carefully, thoughtfully, in a way that others could reuse. Apps would come along and carelessly, recklessly glue together several high quality libraries into a piece of software targeting a general audience. The apps would then harvest all the credit.
What's happening in mathematics right now feels similar. Applications (theorems) were always how one built objective reputation, but libraries (concepts, definitions, boring lemmas) were also rewarded socially within the mathematics community. And individual mathematicians often managed to both build their own libraries, and use them to prove an important result. And then those libraries were sometimes of use in other results.
Bessis asks whether AI Lean proofs will land in Mathlib or Mathslop. Or in my framing: will they be libraries, or applications?
At present they're mostly Mathslop. The proven result is perhaps useful, but the methods employed aren't novel or reusable. I worry that this trend will only worsen, because applications make headlines, and the libraries they used do not. We are not properly incentivizing library development in OSS, or in math, or in infrastructure writ large. There's a serious credit assignment problem here.
What might change this? Once the low hanging fruit is picked, will citation count rise in relative status again? Will we get result fatigue and start to reward legibility — no one cares unless the paper has an accompanying ELI5 tiktok video? A labeling regime that certifies the proof was produced sustainably, organically, by local artisans with no AI additives?