alt Hacker NewsIs that because you were starting from scratch and working alone, though?
Imagine a hypothetical project at the scale of the Linux kernel, with thousands of mathematicians building up organized and well-commented code, standing on each others shoulders.
(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.