Comment by gewetensleegte
2 hours ago
They first do have to show results that are actually useful to any human, though.
Right now, they just created busy work for real mathematicians while snatching away their feeling of accomplishment and discovery.
The only "use" for these results people can claim currently, all rest on the idea that surely better results will follow. Which is why it's being called strip-mining, because you can only keep that up for so long.
What if they just start churning out Lean proofs forever, and the only job left for mathematicians is turning them into human readable proofs, this is definitely a net negative for humanity, because then true progress of mathematics will slow down, because there are more people that like doing mathematics for discovery and accomplishment, than there are people that like doing math homework for the sake of it.
Also I would prefer a world where humans get to have this sense of discovery and accomplishment, instead of what they are trying to turn mathematics into.
Coding used to be a super creative and rewarding thing for me, and now I do 0 of it. Does this mean I produce less code, or hate my job because I can no longer "do the problem solving" that gave me so much joy? No -- it's the opposite on both accounts and I can actually tackle much larger problems now.
If anything, proof abundance should speed up discovery, and mathematics will be fine. What is happening now is just a massive shock to the system so understandably people are upset.
(It's also understandable why AI companies are strip mining open maths problems. "Solve P=NP" is crazy hard, but still a simple prompt, with a verifiable solution. You don't get that this often outside of maths.)