> Sure, we learned if the statement is true or false; but the proof can't be merged into the pure math codebase unless it's completely rebuilt. This is thankless work that humans are unlikely to want to do, and so the "solution" instead risks leaving a desolate patch of land, where existing efforts in extending the codebase lost their motivation.
Are the AI proofs really that hard to refactor? Wouldn't the AI prover get stuck by straying too far from the safety of existing frameworks and not breaking the larger goal into smaller subgoals?
Why is coming up with a better proof (e.g. shorter, more intuitive, more general, connected to existing frameworks) thankless work? How much of this is a problem because of current incentives?
I think the plausible version of this claim is that it's thankless work compared to solving the problem itself. The Quasi-Riemann Hypothesis and Hilbert's 10th problem over Q have both been described as "instant Fields medal worthy, no question asked". Explaining and cleaning up the proof is obviously important, but also quite a bit easier, and we don't really know what future 'Fields medal worthy' achievements might look like.