Comment by dwohnitmok

> Moreover, it seems the prompt included the technique used to solve the problem:

I don't believe this is true. The author sent techniques he used, but I don't believe any of those were ultimately what GPT-5.6 used.

GPT-5.6 also provided the Lean formalization, which was not provided at all by the author.