Explaining Tao's point in software terms: the point of pure mathematics is to build and maintain a high quality "codebase" of theory, definitions and proofs.
"Open problems are lighthouses not destinations" mean that these are currently not well explained by the theories and people should look into extending the codebase on that direction.
The current generation of math AI is not a "good citizen" in that it doesn't try to make the most elegant additions to the shared framework, but will often just rebuild everything from scratch til get to some endpoint.
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.
As with all things AI we can't take more than a 1-3 year horizon, if even that much. Probably AI will become better at respecting and working within the existing theories as it has with large software codebases.
> The current generation of math AI is not a "good citizen" in that it doesn't try to make the most elegant additions to the shared framework, but will often just rebuild everything from scratch til get to some endpoint.
> 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?
> Why is coming up with a better proof (e.g. shorter, more intuitive, more general, connected to existing frameworks) thankless work?
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.
To extend the software analogy, asking mathematicians to decipher LLM-generated math results is like asking programmers to understand computer programs using a decompiler instead of starting from human-comprehensible source code.