[tacomonstrous]

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.

[pfdietz]

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.

[tacomonstrous]

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.

[muldvarp]

> 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]

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]

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.

[QuesnayJr]

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]

> 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]

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.

[Davidzheng]

Sorry last comment was a bit emotional from me, but I do not think it's findable like you say--during my PhD I tried to find some ideals I knew existed in char 2 in 5 variables and low degree and I didn't think I ever got close. 3 variables, 7 degree, coefficients up to 6 is like 6^100 possibilities. You've got to narrow it down somewhat no? Even sparse is intractable I would guess.

I think the solutions which rely on the least amount of theory are the most telling of the AIs being higher in intelligence than humans today already. There's almost no theory to teach someone to understand the cycle double cover conjecture as you say, yet no one finds it. I don't think the conclusion is that it was "easy", but that it was in fact irreducibly difficult in a way that proofs developed with theory are not. Theory gives the human brain abstractions to simplify complex proofs to be understandable at our capacity--I think there are many proofs which probably are not of this form.

But I think our differences hinge on how hard we perceive these solutions to be--I think they are very hard to find!

[Davidzheng]

But actually my feeling is that the final solutions of these last two problems probably is hiding how the AI came up with them! For all we know it used a LOT of theory! As Dolly Parton says "it takes a lot of money to look this cheap" and it takes a lot of intelligence for the proofs to look this dumb. [In high school, I knew of this competition math kid joke where after you derive an inequality with various methods, you use standard results to write the original equations as just a sum-of-squares---like in a "are you stupid, it's >=0 bc it's a sum of squares" sort of way]

[meowface]

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]

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.

[betafj]

If some LLM is able to come up with a simple proof of Fermat's Last Theorem (a solution that Fermat himself could come up with) in the future, would you still say that Fermat's Last Theorem is hard?

[gilgoomesh]

Goldbach's Conjecture is very accessible.

[muldvarp]

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.

[Davidzheng]

next year is a long time away friend

[meowface]

It's so soon that it may be rational to delay certain math and software projects until smarter models arrive

[jasonfarnon]

no, he's right, we're fucked

[Davidzheng]

? 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