alt Hacker NewsThe 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!
Replies
derbOac • today at 6:33 PM
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.
hacklewoodple • today at 8:43 PM
[dead]
It 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.