>The first was a challenge in pure mathematics known as the cap set problem, which is about finding the largest set of points in space where no three points form a straight line.
FunSearch was able to solve this by churning out programs that generate new large cap sets that go beyond the best that mathematicians have come up with.
>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.
It's worth reading the original article; the link is a poor summary.
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.
9 comments
[ 3.4 ms ] story [ 38.0 ms ] threadhttps://news.ycombinator.com/item?id=38643076
>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.