I get your point and agree to some extent, but you can't understand the proof without significant background in Maths so it will just allow mathematicians to solve issues faster than not have the opportunity at all.
Similarly, humans don't need to be involved in scientific advances to benefit. We just need an aligned AI to take over the scientific thought for us. AI is already better than all but the top tier of humans at doing mathematics, it's writing most of the posts on the front page of this website, and it's doing the bulk of programming at many startups.
We can't put this genie back in the bottle.
If people are just doing math to kill time, I don't get why anyone would bother with AI. Do people really enjoy picking through a million lines of generated Lean code, if it's not for any practical use?
Maybe there's two kinds of math that we need? Useful math and navel gazing, and we can hand the first to the machines, and let hobbyists do the second in their free to entertain themselves?
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.
I agree with you on this point in isolation, but I think it's missing an enormous amount of context. Humans can absolutely benefit from science they weren't involved in and don't understand - I have no idea what a "histimine" is but I benefit from my allergy medication in the springtime.
That said, we're already living through a time where, on the whole, measures of intelligence, literacy, critical thinking, etc. are falling (at least in the US). That is a problem, which risks being exacerbated by AI, and the broader point is that we should be figuring out how to use these tools to produce knowledge that benefits humanity while also maintaining incentives for people to use their brains. Going back to my allergies: while I don't understand how my allergy meds work, my life is better, and I'm a better spouse/parent/friend/citizen etc., because I've taken the time to understand how other parts of the scientific and mathematical world that do interest me work. The current AI push to just throw out LLM-generated Lean proofs of everything under the sun to get headlines and pump up their IPO valuations (which this Marathon seems, intentionally or not, to be participating in), doesn't appear to be considering this alignment between what we get from AIs and how we can maintain our incentives to do human science. It seems more like measuring you-know-whats while risking that the message the broader public takes away is that math "has been automated" so what's the point in using your brain anymore?