I also tried to get into it recently, and I feel theorem proving has been pretty substantially oversold. It seems that if you wanted to work through the proofs in even an advanced undergraduate or early graduate textbook, you would basically have publishable material at the end because of the lack of cohesive libraries. There is a lot that gets buried in and is still open to implementation details, and I don't see any clear way of simply proceeding. It started to feel like a major distraction from just doing the mathematics rather than an aid, like it's supposed to be. It feels a little like the Rust ecosystem, where there is a land grab rush to introduce various libraries.
I agree that there's generally too little results in mathlib and for that matter in any theorem prover, but I didn't think that work on formalizing such stuff (advanced undergrad results / early grad results) is publishable. Was I wrong in this?
There's plenty of published papers about newly formalized proofs, even in "undergrad" math. A formal proof development generally brings to light new information about the original proof, both by plugging all potential inaccuracies/missing steps and in being especially easy to refactor, abstracting out common patterns that might be reused elsewhere.
