I find it kind of interesting the whole output wasn't released. A common criticism of mathematical writing is results are "pulled out of a hat"; you only write up a polished, final proof, but hide everything that went into developing it. It's kind of ironic the practice is even carried on when an LLM writes the proof.