[bckgrndrdtn]

You would think that the people maintaining Mathlib are a subset of {understands type theory and how theorem provers work}...

Yet they don't merge this stuff, for many different reasons, including that those 200K lines are free as in puppies.

You can have all the type theory of the world, but the library still needs maintenance.

Change a simp-lemma in a file close to the root. Oooh noes, now there's 987 errors in the 200K loc that we merged last week. And there's nobody there who understands how to fix them.

Just use AI to fix. Or maybe just don't merge the code and let it sit in a downstream library?

And wait until there's evidence that the code is stable, high-quality, with well-designed APIs. And then decide that it might be worthy including in a more foundational library.