As I understand it Lean is not a general purpose programming language, it is a DSL focused on formal logic verification. Bugs in a DSL are generally easier to identify and fix.

It seems one side of this argument desperately needs AI to have failed, and the other side is just saying that it probably worked but it is not as important as presented, that it is actually just a very cool working methodology going forward.

Lean 4 is a bit awkward, but workable as a general purpose programming language, it e.g. supports sockets (with a C module, but so does Python.)