It also links to a paper written by an LLM where the model "reconstructs how the proof came together" based on the unpublished reasoning traces: https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf
I wish they'd publish the prompts though!
I just want to state that having "lean proofs" that build (checks) does not mean the actual real theorems we care about hold. Ignoring lean kernel bugs, ultimately a human (not an agent) has to verify the lean encoded theorem statements (specs/specifications) that the lean proofs are checked against. For non-trivial theorems such as these, this is an arduous and tricky task where even a little mistake could be fatal. AI generated lean encoded theorems can be huge and difficult to understand. I wonder if anyone reputable has audited these specifications.
This is an extraction from that of the actual theorem statement (39 lines): https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d...
As long as you are not missing important information, how you word the prompt does not have any effect.
The signal here is the action of stopping the agent “do something else, this is stupid”, not a tweak to the initial prompt.