3 ms·
> In either case I believe people who can put AI to the most value are the mathematicians themselves The net output of math will increase, and mathematicians
by bwfan123 8d ago
> In either case I believe people who can put AI to the most value are the mathematicians themselves
The net output of math will increase, and mathematicians have more work now to unravel all this, and make it useful. AI plays the role of a monkey in the infinite monkey theorem [1]. We now need an LLM corollary - Something like: A finite number of LLM agents will almost surely find all theorems given an infinite token budget.
[1] https://en.wikipedia.org/wiki/Infinite_monkey_theorem https://en.wikipedia.org/wiki/Infinite_monkey_theorem
- deleted 8d ago[deleted]
- johnsmith1840 8d agolol same with people. "Given infinite thinking time a finite number of humans will solve all theorems" I also love the angle that this was not intelligence just brute force. As if the mathematicians didn't reeaaally want to solve this they were just too lazy to give it a good try. What does AI have to actually do before you realize these things are actually smart?
- alansaber 8d agoMachines have a much higher capacity for work than human beings. Saying that these proofs did not require equivelant intelligence, but benefitted from sheer volume, does not strike me as unreasonable.
- jimmaswell 8d agoIt feels goalpost-movey to downplay exploring a large search space efficiently in regards to "intelligence". If we dug into a human genius's brain and found it was somehow trying out a million ways to solve a a problem at once, no one would seriously suggest the person isn't actually intelligent. And our brains must something like that at some physical level. You can't have a "turtles all the way down" of reasoning - the building blocks must be simpler. It must reduce to something like pathfinding and brute force at some point, weighted by factors in the system and maybe some randomness.
- alansaber 8d agoWe have a romantic view of intelligence, perhaps stemming from intuition within the context of scientific discovery. Given enough intelligence, and enough context, a brilliant person can have a stroke of inspiration that allows them to make a major leap (a-la General Relativity or Fermats last theorem). We haven't seen THAT same capacity from a machine, but we see the more ordinary, unsexy grinding type of progress that represents 99.9% of scientific reality.
- williamcotton 8d agoIs there truly anything new under the sun? Hasn't all of existence alway been here? All math, all physics? We could have merely discovered it. Intuition might be nothing more than combinations of what already exists rather than some sort of divine insight that unlocks previously unknowable mysteries.
- jimmaswell 8d agoAgreed. I don't believe intuition and creativity would be more than pattern recognition, remixing ideas, and trial and error combined with a kind of "genetic algorithm" approach if you deconstructed them into what the brain is actually doing.
- jimmaswell 8d agoI would find it very interesting to train a model on information only available prior to the discovery of e.g. relativity or calculus and see if it can invent it. My intuition is that modern frontiers absolutely could. Not to take away from their brilliance, but Newton and Einstein were brilliant people who also happened to be in the perfect place at the perfect time - there's not so much "low hanging (i.e. approachable by one brilliant individual) but immensely valuable fruit" anymore.
- johnsmith1840 8d agoYes my only point here is that you can argue about the semantics of how smart they really are but they are undeniably smart. Today it cost massive effort but it's possible 10-20yrs from now an AI could solve a problem like this in under an hour with a single thread on a free subscription paid for by serving an ad. These arguments are so weak because you'll then have to make the same one a few years from now when it does something else impossible. The argument only stands if we assume no progress will occur.
- streetfighter64 8d agoFunny that you imagine a future where AI can solve complex math quickly, but humans are still watching ads, for some reason. I just think you and the other guy have different definitions of "smart". There's no denying that LLMs are useful, but I don't know if I'd classify them as "smart". There were probably people in the 80s saying computers were "smart" because they could compute 78971 * 12341 faster than a human. In what sense is a LLM "undeniably smart" but a CPU from the 80s isn't? Or would you define such a CPU as "smart"?
- johnsmith1840 8d agoASI may kill us all 100yrs from now but ads are forever my friend. You're right though they largely are "smart" in the 80's computer sense. This is largely due to continual learning being unsolved. BUT the more you look at them, research, and try experiments there's something there not in a 80s computer. If I had to guess maybe 1-5% of a humans ability but it's there. They are able to do novel things but ever step outside of their distribution takes exponential effort for every small addition. There is a true ability to adapt and learn new things on the fly, things never seen before. That is the the smart part. There something hidden in these things we don't understand that allows novel insights built from in context learning. It's actually measurable in experimental settings but even there it's hard to tease out. I saw it mostly while doing CL training experiments. But I also see it while working with them for coding novel things. But the more power we provide and farther down the road of this we go those 1-5% are things like solving unsolved math problems. No human solved these things. You say brute force, I say it needed massive effort to break out of it's distribution and get those small insights. It's very human like when taken at scale. The scary thing is that scale is getting smaller every day.
- glimshe 8d agoThis isn't necessarily true. There may be proofs so complex, they could exceed the limit of human cognition.
- pfdietz 8d agoThere certainly are such proofs. Even for simple decidable theories we have very large lower bounds on decision complexity (like double exponential), which implies large lower bounds on the function from "length of theorem statement" to "length of shortest proof". For undecidable theories, there is no computable function bounding this blowup from theorem length to proof length (otherwise, the theory would be decidable.)
- srcreigh 8d agoIt's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable. For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable. Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation. Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.
- Timpanzee 8d agoEven if the busy beaver sequence were computable and the halting problem were decidable, Gödel's incompleteness theorems would still prevent all theorems from being solved, regardless of if one used LLMs or not.
- moomin 8d agoPretty sure Gödel’s theorems imply the halting problem if you squint hard enough.
- srcreigh 8d agoI think there's a really important sense in which Godel's argument is not the full story. IIUC, Godel's incompleteness is less about theorems and more about axiomatic systems. Given an axiomatic system, there are statements within it which cannot be proven or disproven. It's relatively unrelated to the platonic ideal of the theorem itself. The statements it considers are axiomatic-system-specific. Another way to view it is, who cares if we can't prove or disprove "This statement is false". Ok, the axiomatic system is incomplete; fine. What's important is can the system prove a real theorem that I care about. The busy beaver computability argument addresses these issues. The problem format is always "For Turing machine T with no input, does T halt?". This format can encode many math problems. And we know already that BB(432) is independent of ZF, aka, there is a 432-state TMs which ZF can't prove or disprove the halting behaviour of. So BB looks at real theorems, ranks them, and we can ask what axiomatic systems can solve them or not. Godel looks at 1 axiomatic system and produces a toy theorem which the system can't solve. That's an extremely important difference! The core issue is that any fixed LLM can only encode so many axiomatic systems in its states, and the fixed systems implies an upper bound in terms of the BB number which it can solve. Godel is only looking at one system at a time, while BB is a way to use a common problem format to rank every axiomatic system on an infinite number line.