They used an LLM which generated millions of programs as part of an evolutionary search. A few of these programs were able to generate the size-512 Cap Set. This isn’t a hugely important problem, but there was preexisting interest in it. I don’t think it was particularly low-hanging fruit; there have been some followup papers using alternative scaffolding and LLMs, and the 512 result is not easy to reproduce.
I’ve also done some work on LLM generation of programs that have solved longstanding open instances of combinatorial design problems: https://arxiv.org/pdf/2501.17725
As noted in the paper though, these do feel a bit more like low-hanging fruit, and these designs probably could have been found by people working to optimize several methods to see if any work. Still, they were recognized open instances, and no one had previously solved before the LLM generated code that constructed the solution.
If this is an example of an LLM proving something, it’s a very non-central example. It was finetuned specifically for mathematics and then used essentially as a program synthesis engine in a larger system that proved the result.
DeepMind can’t just keep running this system and get more theorems out—once the engineers moved on to other projects I haven’t heard anything building on the results.
I think DeepMind’s FunSearch result, showing the existence of a Cap Set of size 512 for n=8, might qualify:
https://www.nature.com/articles/s41586-023-06924-6
They used an LLM which generated millions of programs as part of an evolutionary search. A few of these programs were able to generate the size-512 Cap Set. This isn’t a hugely important problem, but there was preexisting interest in it. I don’t think it was particularly low-hanging fruit; there have been some followup papers using alternative scaffolding and LLMs, and the 512 result is not easy to reproduce.
I’ve also done some work on LLM generation of programs that have solved longstanding open instances of combinatorial design problems:
https://arxiv.org/pdf/2501.17725
As noted in the paper though, these do feel a bit more like low-hanging fruit, and these designs probably could have been found by people working to optimize several methods to see if any work. Still, they were recognized open instances, and no one had previously solved before the LLM generated code that constructed the solution.
If this is an example of an LLM proving something, it’s a very non-central example. It was finetuned specifically for mathematics and then used essentially as a program synthesis engine in a larger system that proved the result.
DeepMind can’t just keep running this system and get more theorems out—once the engineers moved on to other projects I haven’t heard anything building on the results.
I believe AlphaEvlolve built on the results.
Yes, it’s becoming harder to say whether LLMs have discovered anything.