Comment by gwd
14 hours ago
But this is Tao's point: Before, the mechanism by which a proof was verified and communicated and digested by the community was for the person who came up with the grotty, ugly first draft to engage with the community. Now there's nobody to really engage with, so the pipeline from "grotty, ugly draft" to "integrated into humanity's mathematical knowledge" has been broken.
So yeah, probably we should stop saying "X has been solved", and instead say, "A Lean proof for X (or !X) has been generated". That doesn't change the fact that incentives are currently on finding the proof, and once the proof is generated by an AI, there's not currently a good mechanism / incentive structure to move that into the mathematical community. AI is here, so we need to find a new mechanism.
It is not obvious to me that a single canonical human language write-up of a proof is the best output in this new world where write-ups are cheap. A human reader can query an LLM and get explanations of key points tailored to the reader's own background in mathematics.
> A human reader can query an LLM and get explanations of key points tailored to the reader's own background in mathematics
Convenient. To verify my shovel works you must buy…more shovels!