alt Hacker NewsSo you're not going to do it yourself and you want someone else to do it for you? Some mathematician that dedicated their life to understand mathematics must now toil unpaid and unwillingly to understand the AI slop proofs that you want us to be able to understand?
Do the job yourself. And if you can't, that's maybe a hint that you should listen to the people who can.
Who said anything about unpaid? I'm pretty sure professors don't show up just for fun. Our taxes pay them.
I'd be happy to do the job. Actually I still dabble recreationally (clarifying Codex's Lean proofs, even!). But like I said it's one of the most competitive fields on the planet. As you say, you have to dedicate your life to it.
If a slop proof isn't helpful, they don't have to "toil unwillingly to understand it". They can just proceed with the knowledge that the proposition they want to prove 1. is true and 2. is provable, which is already a decent start for motivation. But often LLMs can actually do quite well explaining ideas too in the hands of an expert. Or you can ask them to prove some technical lemma that you think ought to be true, and that could offer insight for the thing you're really interested in, but for which the details are actually not all that interesting to you. You don't have to one-shot "prove RH from the ground up in 50 million lines of Lean."