6 ms·

Speaking as a mathematician, it does seem like we're a bit fucked as a community. Anything that is at all accessible to currently existing methods and mathemati

Speaking as a mathematician, it does seem like we're a bit fucked as a community. Anything that is at all accessible to currently existing methods and mathematical infrastructure is probably going to fall to the frontier models of today, and at this rate of progress it's likely that, already by next year, we'll see new infrastructure being put into place by AI, giving us a world in which a few designated interpreters of the oracle get to 'do' mathematics, while it withers on the vine as an avenue for the exploration of human meaning.

QuesnayJr 2mo ago
I think in the long run mathematicians are probably fucked, but in the short run it's not that bad. All three of the big conjectures solved the answers were at the level where if you had given a grad student the questions and the right background reading there's a good chance they would have solved it. (This example, you could have given an undergraduate good at programming and computer algebra and told them to come up with a counterexample.) At this point the advantage of AI is that it's read the entire mathematical literature, and it doesn't have to worry about wasting its time. The solved problems have all turned out to be surprisingly easy, so the real lesson is that we're bad at judging how hard problems are. Assuming this state of affairs lasts, the medium-term problem is that you learn something when struggling with a problem, even if you don't solve it, and if mathematicians become too reliant on AI the skills they develop through struggle will erode. The long-term problem, of course, is that it seems much more probable that a future model will make mathematicians all obsolete. But so far Fable hasn't. (Anthropic has probably burned a billion tokens on the Riemann hypothesis already, without telling anyone.)
- Davidzheng 2mo ago
  > This example, you could have given an undergraduate good at programming and computer algebra and told them to come up with a counterexample please try go try it. There's no way someone didn't do massive computer algebra searches before today. > All three of the big conjectures solved the answers were at the level where if you had given a grad student the questions and the right background reading there's a good chance they would have solved it. You cannot be serious... why didn't they solve it before then? Do you think no one tried it? What background do you give the double cycle conjecture student after the flow reduction? a linear algebra textbook???
  - QuesnayJr 2mo ago
    Why would I try it to win an argument on HN? That's a bizarre suggestion. Just look at the degree. If it were degree 47 in 17 variables then it wouldn't be surprising, but here it's surprising. Of course people tried hard to solve them all, which is why it's so surprising that they were open. If anything, the solutions have gotten easier. The unit distance graph solution relied on a famous theorem remote from graph theory. The cycle double cover solution relied on a standard theory in graph theory. The solution of the Jacobian conjecture required nothing beyond knowing the definition of the Jacobian. We're just surprisingly bad at judging the difficulty of problems. It's probably something psychological. It's even a known phenomenon, where someone will be stuck on a proof, someone else will announce the result, and the first person will suddenly get unstuck on their proof and produce an independent proof of the same theorem.
    - meowface 2mo ago
      You can use that retroactive logic about any hard problem though. Unsolved murder cases, math, theoretical physics. If tons of smart humans try for years and fail and then an LLM tries for a few weeks or hours and succeeds, the implications are clear. And these are by far the dumbest LLMs will ever be.
      - QuesnayJr 2mo ago
        The retrospective view is important, though. In retrospect, these problems weren't that hard. (The unit distance graph problem was the hardest.) There are some problems that still seem hard, even when we know the answer. Nobody thinks that Fermat's last theorem is easy, even though now know it to be true. Before AI, it was pretty rare that a problem that turned to be unexpectedly easy, so mathematicians thought they were pretty good judges of it. (The last pre-AI example I can remember is the Gaussian correlation conjecture.) So thanks to AI we have learned that we were overconfident in our ability to judge difficulty. If a truly major problem falls, like the Riemann hypothesis, and the proof turns out to be 10 pages, then the lesson will be a different one -- mathematicians are bad at math, and they should turn to more natural domains for them, like folding and putting away towels.
Davidzheng 2mo ago
next year is a long time away friend
- meowface 2mo ago
  It's so soon that it may be rational to delay certain math and software projects until smarter models arrive
- jasonfarnon 2mo ago
  no, he's right, we're fucked
  - Davidzheng 2mo ago
    ? did you take my comment to mean that math will not be affected? I meant like it'll come much sooner--like in <5 months
pfdietz 2mo ago
Proving theorems will have lower payoff, but posing new questions (for AI to chew on) will have higher payoff. Math will go from theorem proving to conjecture farming/exploration. In a way this could be even more fun. Of course AI can also farm conjectures, but they have to develop taste, which might be harder than just proving theorems.
- muldvarp 2mo ago
  > Of course AI can also farm conjectures, but they have to develop taste, which might be harder than just proving theorems. Do you have any argument why you might think this would be true?
  - pfdietz 2mo ago
    For theorem proving, once the statement is formalized, there's an oracle for correctness of the proof. For deciding if something is interesting, well, de gustibus non est disputandum, you know? Experience with Lenat's AM decades ago had it go off making all sorts of uninteresting hypotheses. That's very weak evidence, of course. This suggests people also have role for fundung "beautiful" or "the best" proofs, since that also involves taste. More generally, perhaps the role of people is to reveal their preferences, and that requires people be in the loop somehow. Maybe "math criticism" becomes the job. And if AI is to serve people in general, it needs to know these preferences.
    - muldvarp 2mo ago
      I think the training data contains more than enough information for an LLM to learn what kind of proof is considered beautiful or elegant by humans. Of course it also contains more than enough information to learn what kind of question is interesting to humans.
- tacomonstrous 2mo ago
  Yes, as someone who prefers developing the 'correct' structure over 'merely' proving theorems, this is good for me in the short term. However, the writing I fear is on the wall for my medium and long term utility.
gilgoomesh 2mo ago
Goldbach's Conjecture is very accessible.
muldvarp 2mo ago
Anybody that has to work for a living is fucked and not on the "can't do mathematics which they would find fulfilling"-level but on the "can't afford food, because human intelligence is simply not required anymore"-level.

QuesnayJr 2mo ago

I think in the long run mathematicians are probably fucked, but in the short run it's not that bad. All three of the big conjectures solved the answers were at the level where if you had given a grad student the questions and the right background reading there's a good chance they would have solved it. (This example, you could have given an undergraduate good at programming and computer algebra and told them to come up with a counterexample.) At this point the advantage of AI is that it's read the entire mathematical literature, and it doesn't have to worry about wasting its time. The solved problems have all turned out to be surprisingly easy, so the real lesson is that we're bad at judging how hard problems are. Assuming this state of affairs lasts, the medium-term problem is that you learn something when struggling with a problem, even if you don't solve it, and if mathematicians become too reliant on AI the skills they develop through struggle will erode. The long-term problem, of course, is that it seems much more probable that a future model will make mathematicians all obsolete. But so far Fable hasn't. (Anthropic has probably burned a billion tokens on the Riemann hypothesis already, without telling anyone.)

Davidzheng 2mo ago
> This example, you could have given an undergraduate good at programming and computer algebra and told them to come up with a counterexample please try go try it. There's no way someone didn't do massive computer algebra searches before today. > All three of the big conjectures solved the answers were at the level where if you had given a grad student the questions and the right background reading there's a good chance they would have solved it. You cannot be serious... why didn't they solve it before then? Do you think no one tried it? What background do you give the double cycle conjecture student after the flow reduction? a linear algebra textbook???
- QuesnayJr 2mo ago
  Why would I try it to win an argument on HN? That's a bizarre suggestion. Just look at the degree. If it were degree 47 in 17 variables then it wouldn't be surprising, but here it's surprising. Of course people tried hard to solve them all, which is why it's so surprising that they were open. If anything, the solutions have gotten easier. The unit distance graph solution relied on a famous theorem remote from graph theory. The cycle double cover solution relied on a standard theory in graph theory. The solution of the Jacobian conjecture required nothing beyond knowing the definition of the Jacobian. We're just surprisingly bad at judging the difficulty of problems. It's probably something psychological. It's even a known phenomenon, where someone will be stuck on a proof, someone else will announce the result, and the first person will suddenly get unstuck on their proof and produce an independent proof of the same theorem.
  - meowface 2mo ago
    You can use that retroactive logic about any hard problem though. Unsolved murder cases, math, theoretical physics. If tons of smart humans try for years and fail and then an LLM tries for a few weeks or hours and succeeds, the implications are clear. And these are by far the dumbest LLMs will ever be.
    - QuesnayJr 2mo ago
      The retrospective view is important, though. In retrospect, these problems weren't that hard. (The unit distance graph problem was the hardest.) There are some problems that still seem hard, even when we know the answer. Nobody thinks that Fermat's last theorem is easy, even though now know it to be true. Before AI, it was pretty rare that a problem that turned to be unexpectedly easy, so mathematicians thought they were pretty good judges of it. (The last pre-AI example I can remember is the Gaussian correlation conjecture.) So thanks to AI we have learned that we were overconfident in our ability to judge difficulty. If a truly major problem falls, like the Riemann hypothesis, and the proof turns out to be 10 pages, then the lesson will be a different one -- mathematicians are bad at math, and they should turn to more natural domains for them, like folding and putting away towels.

Davidzheng 2mo ago

next year is a long time away friend

meowface 2mo ago
It's so soon that it may be rational to delay certain math and software projects until smarter models arrive
jasonfarnon 2mo ago
no, he's right, we're fucked
- Davidzheng 2mo ago
  ? did you take my comment to mean that math will not be affected? I meant like it'll come much sooner--like in <5 months

pfdietz 2mo ago

Proving theorems will have lower payoff, but posing new questions (for AI to chew on) will have higher payoff. Math will go from theorem proving to conjecture farming/exploration. In a way this could be even more fun. Of course AI can also farm conjectures, but they have to develop taste, which might be harder than just proving theorems.

muldvarp 2mo ago
> Of course AI can also farm conjectures, but they have to develop taste, which might be harder than just proving theorems. Do you have any argument why you might think this would be true?
- pfdietz 2mo ago
  For theorem proving, once the statement is formalized, there's an oracle for correctness of the proof. For deciding if something is interesting, well, de gustibus non est disputandum, you know? Experience with Lenat's AM decades ago had it go off making all sorts of uninteresting hypotheses. That's very weak evidence, of course. This suggests people also have role for fundung "beautiful" or "the best" proofs, since that also involves taste. More generally, perhaps the role of people is to reveal their preferences, and that requires people be in the loop somehow. Maybe "math criticism" becomes the job. And if AI is to serve people in general, it needs to know these preferences.
  - muldvarp 2mo ago
    I think the training data contains more than enough information for an LLM to learn what kind of proof is considered beautiful or elegant by humans. Of course it also contains more than enough information to learn what kind of question is interesting to humans.
tacomonstrous 2mo ago
Yes, as someone who prefers developing the 'correct' structure over 'merely' proving theorems, this is good for me in the short term. However, the writing I fear is on the wall for my medium and long term utility.

gilgoomesh 2mo ago

Goldbach's Conjecture is very accessible.

muldvarp 2mo ago

Anybody that has to work for a living is fucked and not on the "can't do mathematics which they would find fulfilling"-level but on the "can't afford food, because human intelligence is simply not required anymore"-level.