If we can now throw enough computational at theoretical questions that we can now stochastically "hit-test" generated proofs against a solver until a permutation succeeds, rather than validating a discovered, human crafted proof - and consequently needing to reverse engineer insight or even comprehension out of those generated validations rather than the usual other way around - then math ends up looking like early biochemistry, with the laws physics replaced by the correctness of the solver.
An example occured just today, in which we were treated to the unedifying spectacle of no fewer than three separate AI companies race to announce their own improvement on the bounded gaps between prime result that I mentioned yesterday at https://mathstodon.xyz/@tao/117197525544971208 . These results are numerically stronger than Stadlmann's improvement, but I am very glad that Stadlmann was able to complete her analysis just in time before the problem became contaminated, as the insights that are easily extractable from her paper - in particular, the value of developing equidistribution estimates for numbers with a large smooth factor, as well as reinforcing the use of previous innovations such as the Polymath8b "epsilon enlargement trick" and the Baker-Harman introduction of the Harman sieve, would have been significantly harder to extract in the counterfactual situation in which the AI-generated proofs were released first (without any professionally written writeup to improve the signal-to-noise ratio), and Stadlmann's effort was subsequently abandoned. (3/3)