Comment by staticshock
6 hours ago
When high quality effort is applied to a tool, such as AES or the linux kernel, we intuit that it "hardens" the tool. That is, it makes the tool more correct, more resilient, less assailable, etc.
Similarly, when effort is applied to an open problem, such as the Riemann hypothesis or P v NP, without progress, it "hardens" the problem: it makes the problem feel more daunting to whoever takes a stab at it next.
Andrew Wiles, whose interview also hit the homepage today (https://news.ycombinator.com/item?id=49075264), couldn't just tackle Fermat's Last Theorem head on, he had to wait until a different, modern problem reduced to it, because FLT had gathered this mystique of unassailability through its 300 years of existence.
A thing I worry about is that as AI transmutes tokens into effort, it'll split the world into two: some problems will yield, making human effort entirely unnecessary, and others will harden to the point where human effort will feel increasingly less worthwhile, because "even AI couldn't solve it". I don't like this. AI is spiky, so I suspect it'll continue having major blind spots, and yet its mere presence will probably have a chilling effect on what would have otherwise been useful human effort.
AI is nowhere near the intelligence of a very educated person that has innate talent for problem solving. It does solve the problem of applying human intelligence on problems that truly need it. AI is also a great tool to see if there's something simple that we've missed or just haven't even attempted due to wrong assumptions.
> if there's something simple that we've missed
That's exactly what current mathematicians are using AI for [1].
However, the same mathematicians also believe that pursuing a beautiful proof (even if none exists) is worth it.
[1] https://spectrum.ieee.org/ai-in-mathematics
This is a problem that will solve itself, people will continue to work on the problems that AI fails at, likely by telling AI the approaches they want AI to take.
i think id almost worry more that ai can solve problems in latent space that it cant translate back to tokens because decoding ruins it, and that we wont be able to come up with concepts that we can map to properly decode those solutions in a way people understand
... what is understanding of mathematics anyway? if some AI result helps a mathematician to solve more problems I would say then that it gave them some understanding, but just as there are proofs that span hundreds of pages it's likely that soon proofs will be long Lean programs and studying them will be part of mathematics, just as studying Go played by AI.
(see the open (Lean) label for Erdos problems https://mathstodon.xyz/@tao/116987866420438091)
https://davidbessis.substack.com/p/the-fall-of-the-theorem-e...
This blog post talks in depth about what you're talking about. It may interest you. It even talks about the future where math proofs are just Lean programs, and why that won't necessarily be a good thing.
It's worth a read, even if it's long AF.
I wouldn't worry about too many mathematicians adopting the "even AI couldn't solve it" attitude.
Business folks riding the hype train? Maybe.