[Davidzheng]

P3: interesting that in the basics section, it makes an easy observation but no proof sketch. unlike P1/P2 (P1 has full proof idea sketch P2 says we'll bash). This suggests actually the whole proof is generated one-shot (unlike my previous comment). I guess it's not doing search in the text space (like output some line search for next line etc). OFC there's probably some final process outputing the proof from some parts so it could be obfuscated the search.

come to think of it, informal proof gen probably can't easily use search? Probably it's doing parallel generation with some information sharing + global verification process. No real evidence except for the fact that the entire proof is very unstructured despite at each line it's written with some style consistency.