The GitHub repo with the Lean formalizations just came out a couple of hours ago: 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

I wish they'd publish the prompts though!

▲

derbOac 2 hours ago | parent | next [-]

I 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.

▲

fooker 2 days ago | parent | prev | next [-]

Exact prompts haven't mattered for about a year now.

▲

Alifatisk a day ago | parent [-]

Care 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 a day ago | parent [-]

There'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.

	▲	s4i an hour ago \| parent \| next [-]
		Isn’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.
	▲	Alifatisk 5 hours ago \| parent \| prev [-]
		Oh yeah, I suspected it was something like this. Thanks!

▲

hacklewoodple 3 minutes ago | parent | prev [-]

[dead]