DeepMind's LLM Just Solved an Unsolvable Math Problem
em360tech.com
em360tech.com
>The second puzzle was the bin packing problem about finding the best ways to pack items of different sizes into containers. The problem is typically solved by either packing items into the first bin that has room or into the bin with the least available space where the item will still fit.
>But, according to the researchers’ paper, FunSearch found a better approach by attempting to fill small gaps that were unlikely to ever be filled.
The first of two problems is a generalization to any dimension of finding a maximal non-set in the game of Set. That's lines over Z/3Z. Over R, for n > 1 the same question is obviously unbounded; any finite set of points in general position works. The writer just said "space" and didn't stop to think.
Both problems involve having the computer find interesting examples, not machine-checked proofs, in search spaces too large for brute force. Having AI guide such a search is a worthy endeavor, but it's not the same as a machine spewing out better Lean 4 proofs than people can produce. Soon, we'll be getting such help, but this isn't that. Misleading headline.