4 ms·
The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs https://github.com/openai/ten-proofs It
by simonw 3mo ago
The GitHub repo with the Lean formalizations just came out a couple of hours ago: https://github.com/openai/ten-proofs https://github.com/openai/ten-proofs
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 https://cdn.openai.com/pdf/reasoning-walkthroughs.pdf
I wish they'd publish the prompts though!
- fooker 3mo agoExact prompts haven't mattered for about a year now.
- Alifatisk 3mo agoCare to elaborate? Curious about this. Is this because LLMs have been geared towards understanding user user intent behind a prompt rather than following the instructions exactly?
- fooker 3mo agoThere's a full fledged 'reasoning' step that basically expands your prompt. As long as you are not missing important information, how you word the prompt does not have any effect.
- Alifatisk 3mo agoOh yeah, I suspected it was something like this. Thanks!
- s4i 3mo agoIsn’t that a huge simplification? Of course the way you phrase the prompt can carry semantic meaning, maybe subtly, but still. And sometimes that matters a little and sometimes a lot. I’ve stopped numerous agent sessions over the last few weeks to reword my initial prompt to get the agent off an unintended track.
- fooker 2mo ago> reword my initial prompt to get the agent off an unintended track. The signal here is the action of stopping the agent “do something else, this is stupid”, not a tweak to the initial prompt.
- derbOac 3mo agoI like the Lean formalizations — I hadn't thought seriously of asking for that before but might try it with some stuff I've been working on.
- hacklewoodple 3mo ago[dead]
- rencrisa 3mo agoIt seems that a lot of folks misunderstand the guarantees that lean provides. 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.
- deleted 3mo ago[deleted]
- nilkn 3mo agoThis is the Lean proof that a nonsofic group exists (34,440 lines): https://github.com/openai/ten-proofs/blob/main/NonSoficGroup.lean https://github.com/openai/ten-proofs/blob/main/NonSoficGroup... This is an extraction from that of the actual theorem statement (39 lines): https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6/ComparatorChallenges/D_NonSoficGroup.lean https://github.com/openai/ten-proofs/blob/94bc0feb6a9ff12c7d...
- rencrisa 3mo agoIt may be for this theorem there's a succinct description, but still needs to be checked carefully. However, there are others that are non-trivial.
- nilkn 3mo agoIn some cases you're right, but I think that's often a symptom of mathematics in Lean being relatively immature (i.e., it will get much easier with time). Even then, verifying the statement in Lean is correct is still much easier than verifying the natural language proof is correct.