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.

Would a human be able to see the entire 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.

Perhaps, but due to the slop nature of OpenAI proofs, the proofs remain unaccepted by mathematicians, which leads one to question how many are valid proofs and how many are nonsense. If we see that they are nonsense, then OpenAI has wasted a huge amount of effort in mathematics. Famously the ABC conjecture proof of 500 pages is still unaccepted despite having been written in 2012.

Already people are seeing that the lean proofs provided don’t match the paper and lean proofs have not been provided for all paper proofs.