Comment by mrob

1 day ago

There are many independent implementations of Lean's proof checker:

https://arena.lean-lang.org/

It's highly implausible that the same bug is present in all of them.

4 comments

mrob

Reply
pera  1 day ago

Is that true? I'm actually asking because all the ones that I have seen mentioned from the arena were generated with Claude and I just checked a few random ones and they all have commits by Claude.

I don't know how much was created by LLMs but can you still call these independent implementations?

  • StilesCrisis  21 hours ago

    Yes? Very little about Claude is deterministic. If given the same sufficiently complicated problem, but via slightly different input prompts, it can generate entirely different code. It would be shocking if they all had a single shared bug.

    • Eddy_Viscosity2  20 hours ago

      If it's a complicated but narrow problem then regardless of the prompt its possible that Claude will always converge to the same solution type from its training data. So it will generate different version of the same code that have the different implementations of the same procedure that 'works' but is incorrect in some subtle way.

    • foldr  20 hours ago

      I don't think it would be that shocking, if it's a conceptual confusion that's easy to make.