3 ms·

I don’t get why so many people are resistant to the concept that AI can prove new mathematical theorems. The entire field of math is fractal-like. There are ma

by aabhay 1y ago

I don’t get why so many people are resistant to the concept that AI can prove new mathematical theorems. The entire field of math is fractal-like. There are many, many low hanging fruits everywhere. Much of it is rote and not life changing. A big part of doing “interesting” math is picking what to work on. A more important test is to give an AI access to the entire history of math and have it _decide_ what to work on, and then judge it for both picking an interesting problem and finding a novel solution.

tcshit 1y ago
I like the idea of letting AI try to formulate new math problems that are interesting, i.e. worthy research level. I guess we are still a number of iterations away till AI get there though..
xenotux 1y ago
I think a simple way to take emotion out of this is to ask if a computer can beat humans at math. The answer to that is pretty much "duh". Symbolic solvers and numerical methods outperform humans by a wide margin and allow us to reach fundamentally new frontiers in mathematics. But it's a separate question of whether this is a good example of that. I think there is a certain dishonesty in the tagline. "I asked a computer to improve on the state-of-the-art and it did!". With a buried footnote that the benchmark wasn't actually state-of-the-art, and that an improved solution was already known (albeit structured a bit differently). When you're solving already-solved problems, it's hard to avoid bias, even just in how you ask the question and otherwise nudge the model. I see it a lot in my field: researchers publish revolutionary results that, upon closer inspection, work only for their known-outcome test cases and not much else. Another piece of info we're not getting: why this particular, seemingly obscure problem? Is there something special about it, or is it data dredging (i.e., we tried 1,000 papers and this is the only one where it worked)?
SkyPuncher 1y ago
For me it comes down to signal vs noise. I’m absolutely confident that AI/LLM can solve things, but you have to shift through a lot of crap to get there. Even further, it seems AI/LLM tend to solve novel problems in very unconventional ways. It can be very hard to know if an attempt is doomed, or just one step away from magic.
- teeray 1y ago
  At that point, is it really solving or is it just monkeys with typewriters?
  - fwip 1y ago
    "Monkeys with typewriters," is in one sense, a uniform sampling of the probability space. A brute-force search, even when using structured proof assistants, take a very long time to find any hard proof, because the possibility space is roughly (number of terms) raised to the power of (length of the proof). But similarly to how a computer plays chess, using heuristics to narrow down a vast search space into tractable options, LLMs have the potential to be a smarter way to narrow that search space to find proofs. The big question is whether these heuristics are useful enough, and the proofs they can find valuable enough, to make it worth the effort.
  - myaccountonhn 1y ago
    Or finding the solution hidden somewhere among the decimals of pi.
  - naasking 1y ago
    I think the signal-to-noise is demonstrably higher with AI than with a legion of monkeys on typewriters. I think an interesting philosophical question is, is there some threshold of signal-to-noise that by itself would qualify a system as "intelligent", or is "intelligence" some specific property of the search process itself? eg. perhaps real intelligence avoids certain pitfalls, like getting stuck in local minima.
  - marmakoide 1y ago
    It's stochastic monkeys, but enhanced with a really good bias towards coherent prose, built upon a gigantic corpus.
    - 0points 1y ago
      So, it's monkeys specifically good at typing Shakespeare.
foobarqux 1y ago
As others have said computers already help prove theorems like the four color theorem. It’s not that shocking that LLMs can prove a relative handful of obscure theorems. An alpha-theorem (neural net directed “brute force” search) type system will probably also be able to prove some theorems. There is no evidence today that there will be a massive breakthrough in math due to those systems let alone through LLM type systems. If LLMs were already a breakthrough in proving theorems, even for obscure minor theorems, there would be a massive increase in published papers due to publish or perish academic incentives.
ninetyninenine 1y ago
There are more programmers resistant to the concept of AI because of pride. Programmers take pride in their ability to program and to reduce their own abilities into an algorithm reproducible by an LLM is both an attack on their pride and an attack on their livelihood. It’s the same reason why artists say AI art is utter crap when in a blind folded test they usually won’t be able to tell the difference.
- deleted 1y ago
  [deleted]
hto2i34334324 1y ago
That's not the issue. The issue has always been that of knowledge and epistemology. This is why the computer-assisted proof of the four-color theorem was such a talking point in math/cs-circles: how do you "really" know what was proven. This is slightly different from say an advisor who trains his students : you can often sketch out a proof, even though the details require quite a bit of work.
ComplexSystems 1y ago
People are resistant because: 1. There's this huge misconception that LLMs are literally just memorizing stuff and repeating patterns from their training data 2. People glamorize math and feel like advancements in it would "be AGI" They don't realize that having it generate "new math" is not much harder than having it generate "new programs." Instead of writing something in Python, it's writing something in Lean.
- martin-t 1y ago
  1) They absolutely do sometimes repeat training data verbatim.[0] 2) That's not even the point. The point is being trained on stolen data without permission, pretending that the resulting model of the training data is not a derived work of the training data and that the output of the model plus a prompt is not derived work of the training data. Point 1 is just an extreme edge case which is a symptom of point 2 and yet people still have trouble accepting it. GPL was about user freedom and now if derived work no longer applies as long as you run code through a sufficiently complex plagiarism automator, plagiarism is unprovable and GPL is broken. Great, we lost another freedom. [0]: I recall a study or court document with 100 examples of plagiarising multiple whole paragraphs from the New York Times, don't have time to look for it now
  - danielbarla 1y ago
    You're completely correct in your two points, however people _do_ regularly assert that LLMs cannot possibly generate anything novel: "they are just regurgitating and recombining the original". I mean, sure. But so am I (in what is likely a far more advanced manner, but still). I also find it somewhat funny that I am also partially trained on stolen data without permission. I also jaywalk occasionally (perhaps I am trivializing the topic too much, but show me a researcher who hasn't _once_ downloaded a paper they really needed, in less than perfectly legal ways).
    - martin-t 1y ago
      Human time is valuable, LLM time is not. If you spend hundreds of hours creating something, nobody should have the right to copy (verbatim or with automatic modifications) it unless you allow them. Human rights are valuable. LLMs allow laundering GPL code (removing both attribution and users' rights to inspect and modify the code). Free software cannot compete against proprietary in a world where making a copy is trivial but proving it's a copy is nearly impossible.
_Algernon_ 1y ago
A monkey hammering gibberish on a keyboard can prove new math given sufficient time. That's a low bar to set. The question is if the signal-to-noise ratio is high enough for it to be worthwhile.
trueismywork 1y ago
People are not resistant to that concept. People are resistant to OpenAI making ehse claims without proper science practices. https://mathstodon.xyz/@tao/114881418225852441 https://mathstodon.xyz/@tao/114881418225852441 https://mashable.com/article/openai-claims-gold-medal-performance-imo-drama-ensues https://mashable.com/article/openai-claims-gold-medal-perfor... Note that no one expressed skepticism of what google said when they claimed they achieved gold medal. But no one is willing to believe OpenAI.
throwawaymaths 1y ago
or, just put AI on the collatz conjecture.

by aabhay 1y ago

tcshit 1y ago

I like the idea of letting AI try to formulate new math problems that are interesting, i.e. worthy research level. I guess we are still a number of iterations away till AI get there though..

xenotux 1y ago

I think a simple way to take emotion out of this is to ask if a computer can beat humans at math. The answer to that is pretty much "duh". Symbolic solvers and numerical methods outperform humans by a wide margin and allow us to reach fundamentally new frontiers in mathematics. But it's a separate question of whether this is a good example of that. I think there is a certain dishonesty in the tagline. "I asked a computer to improve on the state-of-the-art and it did!". With a buried footnote that the benchmark wasn't actually state-of-the-art, and that an improved solution was already known (albeit structured a bit differently). When you're solving already-solved problems, it's hard to avoid bias, even just in how you ask the question and otherwise nudge the model. I see it a lot in my field: researchers publish revolutionary results that, upon closer inspection, work only for their known-outcome test cases and not much else. Another piece of info we're not getting: why this particular, seemingly obscure problem? Is there something special about it, or is it data dredging (i.e., we tried 1,000 papers and this is the only one where it worked)?

SkyPuncher 1y ago

For me it comes down to signal vs noise. I’m absolutely confident that AI/LLM can solve things, but you have to shift through a lot of crap to get there. Even further, it seems AI/LLM tend to solve novel problems in very unconventional ways. It can be very hard to know if an attempt is doomed, or just one step away from magic.

teeray 1y ago
At that point, is it really solving or is it just monkeys with typewriters?
- fwip 1y ago
  "Monkeys with typewriters," is in one sense, a uniform sampling of the probability space. A brute-force search, even when using structured proof assistants, take a very long time to find any hard proof, because the possibility space is roughly (number of terms) raised to the power of (length of the proof). But similarly to how a computer plays chess, using heuristics to narrow down a vast search space into tractable options, LLMs have the potential to be a smarter way to narrow that search space to find proofs. The big question is whether these heuristics are useful enough, and the proofs they can find valuable enough, to make it worth the effort.
- myaccountonhn 1y ago
  Or finding the solution hidden somewhere among the decimals of pi.
- naasking 1y ago
  I think the signal-to-noise is demonstrably higher with AI than with a legion of monkeys on typewriters. I think an interesting philosophical question is, is there some threshold of signal-to-noise that by itself would qualify a system as "intelligent", or is "intelligence" some specific property of the search process itself? eg. perhaps real intelligence avoids certain pitfalls, like getting stuck in local minima.
- marmakoide 1y ago
  It's stochastic monkeys, but enhanced with a really good bias towards coherent prose, built upon a gigantic corpus.
  - 0points 1y ago
    So, it's monkeys specifically good at typing Shakespeare.

foobarqux 1y ago

As others have said computers already help prove theorems like the four color theorem. It’s not that shocking that LLMs can prove a relative handful of obscure theorems. An alpha-theorem (neural net directed “brute force” search) type system will probably also be able to prove some theorems. There is no evidence today that there will be a massive breakthrough in math due to those systems let alone through LLM type systems. If LLMs were already a breakthrough in proving theorems, even for obscure minor theorems, there would be a massive increase in published papers due to publish or perish academic incentives.

ninetyninenine 1y ago

There are more programmers resistant to the concept of AI because of pride. Programmers take pride in their ability to program and to reduce their own abilities into an algorithm reproducible by an LLM is both an attack on their pride and an attack on their livelihood. It’s the same reason why artists say AI art is utter crap when in a blind folded test they usually won’t be able to tell the difference.

deleted 1y ago
[deleted]

hto2i34334324 1y ago

That's not the issue. The issue has always been that of knowledge and epistemology. This is why the computer-assisted proof of the four-color theorem was such a talking point in math/cs-circles: how do you "really" know what was proven. This is slightly different from say an advisor who trains his students : you can often sketch out a proof, even though the details require quite a bit of work.

ComplexSystems 1y ago

People are resistant because: 1. There's this huge misconception that LLMs are literally just memorizing stuff and repeating patterns from their training data 2. People glamorize math and feel like advancements in it would "be AGI" They don't realize that having it generate "new math" is not much harder than having it generate "new programs." Instead of writing something in Python, it's writing something in Lean.

martin-t 1y ago
1) They absolutely do sometimes repeat training data verbatim.[0] 2) That's not even the point. The point is being trained on stolen data without permission, pretending that the resulting model of the training data is not a derived work of the training data and that the output of the model plus a prompt is not derived work of the training data. Point 1 is just an extreme edge case which is a symptom of point 2 and yet people still have trouble accepting it. GPL was about user freedom and now if derived work no longer applies as long as you run code through a sufficiently complex plagiarism automator, plagiarism is unprovable and GPL is broken. Great, we lost another freedom. [0]: I recall a study or court document with 100 examples of plagiarising multiple whole paragraphs from the New York Times, don't have time to look for it now
- danielbarla 1y ago
  You're completely correct in your two points, however people _do_ regularly assert that LLMs cannot possibly generate anything novel: "they are just regurgitating and recombining the original". I mean, sure. But so am I (in what is likely a far more advanced manner, but still). I also find it somewhat funny that I am also partially trained on stolen data without permission. I also jaywalk occasionally (perhaps I am trivializing the topic too much, but show me a researcher who hasn't _once_ downloaded a paper they really needed, in less than perfectly legal ways).
  - martin-t 1y ago
    Human time is valuable, LLM time is not. If you spend hundreds of hours creating something, nobody should have the right to copy (verbatim or with automatic modifications) it unless you allow them. Human rights are valuable. LLMs allow laundering GPL code (removing both attribution and users' rights to inspect and modify the code). Free software cannot compete against proprietary in a world where making a copy is trivial but proving it's a copy is nearly impossible.

_Algernon_ 1y ago

A monkey hammering gibberish on a keyboard can prove new math given sufficient time. That's a low bar to set. The question is if the signal-to-noise ratio is high enough for it to be worthwhile.

trueismywork 1y ago

People are not resistant to that concept. People are resistant to OpenAI making ehse claims without proper science practices. https://mathstodon.xyz/@tao/114881418225852441 https://mathstodon.xyz/@tao/114881418225852441 https://mashable.com/article/openai-claims-gold-medal-performance-imo-drama-ensues https://mashable.com/article/openai-claims-gold-medal-perfor... Note that no one expressed skepticism of what google said when they claimed they achieved gold medal. But no one is willing to believe OpenAI.

throwawaymaths 1y ago

or, just put AI on the collatz conjecture.