> Fable 5.2 started from minimal prompts, built its own ways to coordinate, and used no mathematical references, only a list of intermediate theorem statements to score progress. It needed one-third of the action tokens as our first formalization and produced a proof seven times shorter.

Is this really so astonishing, assuming that the 5.2 training data certainly had the 'traces' from the Fable original run in it's training data.