Comment by DroneBetter

the proofs written by ChatGPT are necessarily reasoned about in plain language, and are a human-comprehensible length (that is what Tao did, since it hasn't been formalised in a proof-checking language); today, the many-gigabytes (or -terabytes) proofs (à la 4-colour theorem) are generally problems solved via SAT solvers that are required to prove nonexistence of smaller solutions by exhaustion.

and there is an ongoing literature review (which has been lucrative to both erdosproblems and the OEIS), and this one was relabelled upon the discovery of an earlier resolution