Why re-formalise Fermat's Last Theorem instead of doing something new? It's obviously an improvement, but it's an odd thing to boast about as opposed to a novel formalisation or proof.

It's how RLVR works, when you have a task with a verified answer, you rerun the model on it and promote the reasoning chains that reach the answer. That way you can hill climb model capabilities on any problem you find, which generalises to new problems to solve, which you can then hill climb again and so on.

So since they are doing that task anyway (re-solving the problem increasingly more efficiently), this is a easy check point to publish to show how far they've gotten in that process.

... as a test / benchmark? Hard to make a comparison without a control...