(not a mathematician, but I played with lean as a hobby). No, this already existed - lean standard library was basically this, with hundreds of mathematicians working together to formalize basics of currently known math. But this is just very slow for a human.

I remember there being whole research groups trying to formalize a single (real world, as opposed to undergraduate) proof, and I remember reading that formalizing something like FLT is currently completely unfeasible.

In short, no, lean was not a tool to discover new math.