News for hackers. Stuff that matters.
Re:The recently proposed o(n log n) integer multiplication a... by mrob on Thursday October 22, 2026 @04:56AM (#50192938)
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.

Re:The recently proposed o(n log n) integer multiplication a... by pera on Thursday October 22, 2026 @06:39AM (#50193575)
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?

Re:The recently proposed o(n log n) integer multiplication a... by StilesCrisis on Thursday October 22, 2026 @07:43AM (#50194017)
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.
Re:The recently proposed o(n log n) integer multiplication a... by foldr on Thursday October 22, 2026 @08:25AM (#50194367)
I don't think it would be that shocking, if it's a conceptual confusion that's easy to make.
Re:The recently proposed o(n log n) integer multiplication a... by Eddy_Viscosity2 on Thursday October 22, 2026 @09:06AM (#50194794)
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.