This reminds me a lot of the proof by construction for the 4-color theorem. It was only enabled by the advancement of computers and dissatisfied many of the computer scientists and mathematicians since it was a "brute force" approach.

I wonder if AI will end up being similar. Certain theorems get proven by AI but others do not. We haven't reached the limits of this yet and I haven't found a good argument for where those limits will be (I do doubt that there are no limits).