> The biggest benefit of a formalized theorem library is not [...] but [...]
[citation needed]
I think there are many benefits. Hard to claim that your favourite one is the biggest benefit.
In general, I think it's a bit weird that you are repeatedly (also other HN threads, and sibling comments in this one) making unfounded claims about Lean/mathlib, to the point where you are telling maintainers how their system works. And if they explain that you are misunderstanding the system, you ignore their correction and bring up the next (or the same) unfounded claim.