Google DeepMind used a large language model to solve an unsolvable math problem
www.technologyreview.com
They had to throw away most of what it produced but there was gold among the garbage.

The researchers started by sketching out the problem they wanted to solve in Python, a popular programming language. But they left out the lines in the program that would specify how to solve it. That is where FunSearch comes in. It gets Codey to fill in the blanks—in effect, to suggest code that will solve the problem.

A second algorithm then checks and scores what Codey comes up with. The best suggestions—even if not yet correct—are saved and given back to Codey, which tries to complete the program again. “Many will be nonsensical, some will be sensible, and a few will be truly inspired,” says Kohli. “You take those truly inspired ones and you say, ‘Okay, take these ones and repeat.’”

After a couple of million suggestions and a few dozen repetitions of the overall process—which took a few days—FunSearch was able to come up with code that produced a correct and previously unknown solution to the cap set problem, which involves finding the largest size of a certain type of set. Imagine plotting dots on graph paper. The cap set problem is like trying to figure out how many dots you can put down without three of them ever forming a straight line.

  • @thesmokingman@programming.devEnglish
    30•11 months ago

    Buried the fucking lede with misleading garbage. They came up with new, larger cap sets than were previously known. That’s cool, but it doesn’t actually prove anything related to open cap set conjectures. I’d contend this is similar to the early solutions of the four-color map theorem albeit built with a computer coming up with the models to brute force. Pretty fucking neat; not solving an unsolvable problem by any stretch of the imagination. I would expect that kind of hyperbole from the lay press not the fucking MIT Review.

    Edit because this shit is really cool: I intentionally linked this to the four color map theorem because that was the first brute force proof (at least via computer). Lots of people got pissed at the authors and said it was invalid because they reduced their special cases to a finite set and had a computer chug through them. imo proof by computer is valid and one of the ways stuff like this can aid math. There are so many problems in combinatorics alone that could benefit from this treatment of just getting new, unknown special cases to get to a general case or handling previously too large finite sets of special cases.