First I have to say this is sooner than expected, even though I never doubted that this could be done. I am grateful that they dedicated resources to accomplish this. It is clear that agents are very good at discerning and holding onto very weak signals from RL traing on long horizon tasks, so much so that in my own experience even very chaotic agent thinking can converge to meaningful solutions if there is a verifier. I have not dug through the proof yet so I don't know how readable it is to a human. But it has been a dream of mine to understand the FLT proof. I think LLMs will be a big part of making it truly accessible to humans.