But formalization is the easy part for humans. I'm sure every mathematician would be be happy if the only thing required to prove a result was to formalize it in Lean and feed it to the AI to find the proof.
Not sure every mathematician would be happy to do this... it sounds much less pleasant than thinking. It's like saying mathematicians would rather be programmers lol. It's a significant difficult problem which i believe should be left completely to AI. Human formalization should become dead