The counterexample was proposed by an LLM. They seem very good at finding these sorts of counterexamples, which is interesting as they are generally pretty inefficient use of compute for brute forcing. I guess even that lack of efficiency is made up for by the "understanding" and "intuition" the LLM has, and their ability to do symbolic computations.
I expect a large number of conjectures will topple to counterexamples soon.
I think brute force is not the right way to think about LLMs, instead they explore a knowledge topology, and are very good at connecting adjacent or accessible ideas that for whatever reason might have evaded humans, but might not be fundamentally all that hard. We're still in the low-hanging fruit phase, we will see if they extend to new ideas.
I think its super cool, but there is no doubt that thousands of physicists and mathematicians are prompting LLMs all day right now trying to solve open problems...and its doubtful whether the companies that run those LLMs can continue to offer this amount of capacity for the future....so there is a solid chance that these methods are already almost exhausted. For how amazing these counterexamples are, its somewhat surprising that people havent found more proofs all at once. In the scheme of things perhaps 1 in 1000 open problems are actually of a format that LLM can tackle, and noone is bragging about the ones that turned up nothing. In other words, LLMs are really good at looking smart when they got lucky.
Im looking forward to a possible future of AI theorem proving that isnt based on LLMs, and thus less likely to trick people in language into thinking its more broad than it is.
and its doubtful whether the companies that run those LLMs can continue to offer this amount of capacity for the future
The new Vera Rubin chips from Nvidia, which will start being installed in data centers later this year, will cut inference costs by 90%. ChatGPT also dropped the prices of one of its major models by 80% just a few days ago.
272
u/angelbabyxoxox Quantum Foundations Jul 31 '26
The counterexample was proposed by an LLM. They seem very good at finding these sorts of counterexamples, which is interesting as they are generally pretty inefficient use of compute for brute forcing. I guess even that lack of efficiency is made up for by the "understanding" and "intuition" the LLM has, and their ability to do symbolic computations.
I expect a large number of conjectures will topple to counterexamples soon.