P1 has in setup section basically a very precise summary of proof which it fills in later "So main is: (a) for n>=4, any n-line cover must contain a side-line;

P1 has in setup section basically a very precise summary of proof which it fills in later "So main is: (a) for n>=4, any n-line cover must contain a side-line; inductively reduce to n=3. (b) Analyze n=3 exactly." I suspect there's some (tree-based?) search + separate process verifier + large # of parallel generation sessions. Coming just from hints of how structured/monotone the generated text is. A lot of colons. like So: Now: Need: etc..