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.

This is the Lean proof that a nonsofic group exists (34,440 lines): 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/94bc0feb6a9ff12c7d...

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

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

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

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?

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.

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.

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

Oh yeah, I suspected it was something like this. Thanks!

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.