To some extend it is countering Carl Friedrich Gauss' approach of "No self-respecting architect leaves the scaffolding in place after completing his building".

Yet, that way we abstract a proof - compare with a programming library that can be used "as it is" but there is not as much insight into details.

Oftentimes, such scaffolding is didactic - allows to us to learn why a given path was taken, why a "simpler" or "more straightforward" approach didn't work. I would be something like "negative results" in mathematics, no in terms we proved negative, but for some reasons a different approach does not work. Sometimes it is also good for grounding intuition of sorts.

Vide https://mathoverflow.net/questions/459252/when-has-the-scaff...

I have often wondered how long you could string along a mathematician if you started off like many (bad) textbooks from 50 years ago: rattling out a few definitions, proving a few trivial things about them, then making up a couple of new ones and do it again, maybe very tangentially tying it to something previously mentioned, and carefully obfuscate that the definitions and lemmas aren't really going anywhere.

I have long wanted to read firmly motivation-transparent mathematics. They can be abstract nonsense, but it has to be motivated abstract nonsense, you have to tell me what abstract nonsense result you seek and how you plan to go about getting it!

I'm almost offended at the author justifying the need for this database by AI. Yeah, you bet de-obfuscating motivations will help AI, but it will help me too!