One real limitation is context size. 1M tokens is enough to do a lot, but the Lean graphs they are making are way too big to fit, so an LLM will never have the complete picture.
Nope. That's why a lot of knowledge comes down to compressing large concepts into chunks we can understand from new ideas and concepts. LLM's don't tend to be very good and synthesizing such concepts.
No, and that's one of the reasons mathematicians dislike automated solutions. Sure, it's verifiable, but it's too complex and messy to actually learn anything useful. So it technically answers the question, but doesn't leave you with any deeper understanding.