Yes, so if there's useful math, you throw the LLM at it and use the results, no humans needed.

Humans can try to extract some ideas from the million line lean proofs, if they want to, I guess. But I can't imagine anyone really funding the human part of it.