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.