Lean has Claude contributions, what do you expect!
Use Coq or Isabelle or any other decent theorem prover. Lean is just hyped.
Lean has Claude contributions, what do you expect!
Use Coq or Isabelle or any other decent theorem prover. Lean is just hyped.
The relevant kernel code isn't written by Claude though. According to git blame, 95% of the code in inductive.cpp is 5+ years old, with only ~3 hunks (totaling less than 30 lines) coming within the last 12 months including this fix. The Lean kernel in general does not seem to change very much, e.g. the last two years are very sparse in terms of activity with relatively contained changes when I examine the history (especially so when contrasted with the pace of the rest of the project).
Beyond that it looks like a pretty simple oversight. Coq and Isabelle have also had 'prove False' bugs, it isn't the end of the world. Stuff like this happens.
Yeah people don't seem to get that the whole point of having a tightly checked kernel is so you don't have to care so much about the rest of it. Tactic heavy proofs have been "slop" long before LLMs got involved, and they lean heavily on the kernel rejecting nonsense.
What is the error rate of human programmers? Anyone who tells you that either human or A.I. code is magically exempt from issues is selling you something.
There are humans who make very few mistakes. The presence of Claude in a project however tells you something about the attitude of the project:
- Probably too close to corporations.
- Does not care about slop.
We have seen many projects that adopted AI under corporate pressure circle the drain. Often the corporations themselves backpedaled after some months.
> We have seen many projects that adopted AI under corporate pressure circle the drain.
Which?
> Often the corporations themselves backpedaled after some months.
Which
> There are humans who make very few mistakes
Mmm there are humans who think they make very few mistakes. Ones who actually make few mistakes, not sure about that one. Could be a mistake that they catch themselves very quickly, but I just don’t think humans are very good at generating 100% reliable output on the first try anywhere close to most of the time.
Why can’t your two criteria be applied to projects with human contributors without further due diligence?
Claude can produce code that is professionally reviewed and found to be correct.
Do you have any evidence that the bugs were due to LLM code? Or are you just speculating baselessly