Comment by mooreat
3 hours ago
I think one interesting thing to point out is that the proof (disproof) was done by finding a counterexample of Erdős' original conjecture.
I agree with one of the mathematician's responses in the linked PDF that this is somewhat less interesting than proving the actual conjecture was true.
In my eyes proving the conjecture true requires a bit more theory crafting. You have to explain why the conjecture is correct by grounding it in a larger theory while with the counterexample the model has to just perform a more advanced form of search to find the correct construction.
Obviously this search is impressive not naive and requires many steps along the way to prove connections to the counterexample, but instead of developing new deep mathematics the model is still just connecting existing ideas.
Not to discount this monumental achievement. I think we're really getting somewhere! To me, and this is just vibes based, I think the models aren't far from being able to theory craft in such a way that they could prove more complicated conjectures that require developing new mathematics. I think that's just a matter of having them able to work on longer and longer time horizons.
Searching for a proof and disproof are sometimes not so different. In most cases, you nibble the borders to simplify the problem.
For example, to prove something is impossible let's say you first prove that there are only 5 families, and 4 of them are impossible. So now 80% of the problem is solved! :) If you are looking for counterexamples, the search is reduced 80% too. In both cases it may be useful
In counterexamples you can make guess and leaps and if it works it's fine. This is not possible for a proof.
On the other hand, once you have found a counterexample it's usual to hide the dead ends you discarded.
I agree there can be some theory crafting in the search for a counterexample, but in general I think it is easier to search for.
For proving a proposition P I have to show for all x P(x), but for contradiction I only have to show that there exists an x such that not P(x).
While I agree there could be a lot of theory crafting to reduce the search space of possible x's to find not P(x), but with for all x P(x) you have to be able to produce a larger framework that explains why no counter example exists.
> I think that's just a matter of having them able to work on longer and longer time horizons.
No this will never do the kind of math that humans did when coming up with complex numbers, or hell just regular numbers ex nihilo. No matter how long it's given to combine things in its training data.
I currently operate under the assumption that humans are at most as powerful as Turing Machines. And from what I understand these models internally are modeling increasingly harder and larger DFAs, so they're at least as powerful as regular languages.
Assuming humans are more powerful than regular languages I could maybe agree that these methods may not eventually yield entirely human like intelligence, but just better and better approximations.
The vibe I get though is that we aren't more powerful than regular languages, cause human beings feel computationally bounded. So I could see given enough "human signal" these things could learn to imitate us precisely.
Well yeah there is likely an equivalence between computability and epistemology, but I'm not sure it matters when comparing LLM intelligence to human intelligence. There is clearly a missing link that prevents the LLM from reaching beyond its training data the way humans do.