For every important match problem solved by AI, without mathematicians we wouldn't know about the existence and importance of the problem.
Famous mathematical conjectures are social constructs, formed by decades of even centuries of attention given to them by members of the math community. Without it, the danger is that future math "progress" will be reduced to generating tables of Lean statements and a probable/unprovable bit generated by AI.
You make a good point about LLMs being (so far) great at identifying solutions to complex puzzles but not yet coming up with their own theories, questions, etc. The business of finding interesting questions to answer rather than answering them is the essence of what scientists do. Good science identifies more questions than it answers.
With Fermat's theorem, the genius was in the original theorem. Which then caused generations of mathematicians to break their heads over trying to prove it correct. Fermat didn't write down a proof. His theorem was famously just a scribble in a side line of a book. Probably it was something that he had an hunch about that he couldn't quickly falsify.
I don't think AI is being used much for coming up with new problems yet. But I don't see why that would not be possible either. It's the obvious next frontier after AI clears the backlog of existing theorems. I imagine scientists are already using AI to find new interesting problems to work on and generally explore the problem space. But fundamentally, the reflex of asking or imagining "if this is true, what else could be true" is something that distinguishes people from AIs. For now at least.
unddoch · · focus · HN ↗
Famous mathematical conjectures are social constructs, formed by decades of even centuries of attention given to them by members of the math community. Without it, the danger is that future math "progress" will be reduced to generating tables of Lean statements and a probable/unprovable bit generated by AI.
jillesvangurp · · focus · HN ↗
With Fermat's theorem, the genius was in the original theorem. Which then caused generations of mathematicians to break their heads over trying to prove it correct. Fermat didn't write down a proof. His theorem was famously just a scribble in a side line of a book. Probably it was something that he had an hunch about that he couldn't quickly falsify.
I don't think AI is being used much for coming up with new problems yet. But I don't see why that would not be possible either. It's the obvious next frontier after AI clears the backlog of existing theorems. I imagine scientists are already using AI to find new interesting problems to work on and generally explore the problem space. But fundamentally, the reflex of asking or imagining "if this is true, what else could be true" is something that distinguishes people from AIs. For now at least.