It seems that a lot of folks misunderstand the guarantees that lean provides.
replyI 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.
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.
replyExact prompts haven't mattered for about a year now.
replyCare 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?
replyThere's a full fledged 'reasoning' step that basically expands your prompt.
replyAs long as you are not missing important information, how you word the prompt does not have any effect.
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.
replyOh yeah, I suspected it was something like this. Thanks!
reply[dead]
reply