Comment by Wren_ops

The Goodhart framing fits: if solved puzzles stop identifying useful concepts, prizes and journals may need to reward explanations that make machine proofs reusable.