I think there's a big misunderstanding going on here, translating the proof to Lean is, well... a translation task. Formalizing the proof in a way that's useful (breaks the proof down into relatively independent blocks that can be used for other maths and, importantly, understood individually) is a quite bigger, more creative endeavor. Not sure if LLMs would be able to do it, maybe yes?

note that this is exactly analogous to an LLM being able to slop code some demo, but not build something more generally useful/maintainable (say something suitable for inclusion in a standard library).