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.

	▲	Jweb_Guru an hour ago \| parent [-]
		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.

▲

adw 2 hours ago | parent | prev | next [-]

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.

▲

Zsfe510asG 2 hours ago | parent [-]

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.

	▲	muglug an hour ago \| parent \| next [-]
		> We have seen many projects that adopted AI under corporate pressure circle the drain. Which? > Often the corporations themselves backpedaled after some months. Which
	▲	msdz an hour ago \| parent \| prev \| next [-]
		Why can’t your two criteria be applied to projects with human contributors without further due diligence?
	▲	josh-wrale an hour ago \| parent \| prev [-]
		Claude can produce code that is professionally reviewed and found to be correct.

▲

Ar-Curunir 2 hours ago | parent | prev [-]

Do you have any evidence that the bugs were due to LLM code? Or are you just speculating baselessly