In my experience they write an informal proof first, check it without Lean, and only then turn it into Lean code. What they're truly bad at is explaining their proofs. Until they improve at that, we'll have to keep asking Lean whether they solved something correctly.

While they're not great at explaining their own proofs, some models are good at explaining older, human-written proofs.

I definitely don't know but I got the impression it's the opposite. Based on the observations about Navier Stokes and the natural language proof not matching up with the lean proof and other things. They generate lean and convert it into natural language at the end. But really I could be wrong just giving anyone interested a lead to check out.

You cannot brute force lean proofs of any complexity. The space is infinitely large.