Comment by lg5689
8 hours ago
As for #2, personally I feel like OpenAI's results are superhuman at this point. I don't think there's enough human talent alive right now to produce these sorts of results within a few years, no matter the budget.
There are lots of reasons I believe this. One is that frontier AIs are very clearly superhuman on shorter problems (as can be seen on benchmarks like FrontierMath, or just by playing with them yourself if you have a source for difficult problems)--so these achievements are "just" scaling that advantage to research-sized problems. Second, AI is also clearly superhuman in its knowledge across fields, so it can make connections and combine techniques that humans won't be able to access. Third, these problems are famous and have withstood efforts of many of the best humans, in many cases being considered unapproachable.
Altogether it seems like AI is not only smarter but also more cost efficient that humans for math-adjacemt problem solving. I'm not saying that AI is superior at everything in math, eg theory building, but I think it's really unlikely you could get any group of humans that could compete with OpenAI's latest results.
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.)
It depends on the definition of superhuman. For example my car is superhuman as it allows me to get in one hour to a place where it would take me ten hours to go by walking, and can I walk ten hours non stop? However it is not superhuman enough to carry me where I could not walk too. And there are places where I can walk to but I cannot reach by car. Maybe that applies to AIs as well. A plane is in the same category of superhumanity of cars, with more speed. But I could still get to Australia by walking and rowing with my hands on a log (and probably die, I know.)
However there are truly superhuman vehicles, spaceships and submarines, that can carry humans where no human could go alive.
I don't know if these AIs are superhuman in the way of planes or in the way of spaceships. I also don't know if they can do everything we can do by talking or if they have some limits.
I mean, a plane can fly but not reach a branch and stay still on it. A small drone, almost. My coding agents sometimes can't do the obvious but is it because of some intrinsic limitation or because my instructions are bad? So far my experience is that they are superhuman like cars or trains, not yet as planes.
Disproving big conjectures can be useful to mathematicans because it means they don’t have to waste time proving results that assume that conjecture.
Sometimes the very attempt to disprove a conjecture will produce new insights along the way. To get comparable value when a machine simply spits a counterexample, you'd need to at least mine the intermediate reasoning traces to see its false starts.