Hacker News Reader

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

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

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?

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.

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

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.

Reply on news.ycombinator.com