To be fair I think the idea of using algebraic number theory to approach the problem had been tried before (Tsimerman mentions he tried a similar approach that the model ultimately succeeded with, but didn’t persist with it.) It’s quite a general trick to use algebraic number theory for constructions in the plane, as you have the lattice associated with the ring of integers of number fields.
I personally am blown away by the proof but it would be far more impressive had it come up with a novel connection between fields, or indeed if it had turned out there wasn’t a counterexample and it proved a tight upper bound (See Gowers’ initial reaction.)
Also, it disproved it by finding a counterexample, which some have said is less interesting than if it had shown the conjecture was true. I have no familiarity with the problem and can’t judge.
Generally, constructing counterexamples is more amenable to AI automation than constructing positive proofs, because it’s more parallelizable. I think P(AI disproves this conjecture | conjecture is false) would’ve been greater than P(AI proves this conjecture | conjecture is true), given the priors of the mathematicians.
Other info from the announcement worth mentioning:
was a general model, not specialized, they were just testing it on random Erdos problems
key trick seemingly was applying algebraic number theory to geometry in an unexpected way
To be fair I think the idea of using algebraic number theory to approach the problem had been tried before (Tsimerman mentions he tried a similar approach that the model ultimately succeeded with, but didn’t persist with it.) It’s quite a general trick to use algebraic number theory for constructions in the plane, as you have the lattice associated with the ring of integers of number fields.
I personally am blown away by the proof but it would be far more impressive had it come up with a novel connection between fields, or indeed if it had turned out there wasn’t a counterexample and it proved a tight upper bound (See Gowers’ initial reaction.)
Also, it disproved it by finding a counterexample, which some have said is less interesting than if it had shown the conjecture was true. I have no familiarity with the problem and can’t judge.
Generally, constructing counterexamples is more amenable to AI automation than constructing positive proofs, because it’s more parallelizable. I think P(AI disproves this conjecture | conjecture is false) would’ve been greater than P(AI proves this conjecture | conjecture is true), given the priors of the mathematicians.