Lean is a great idea, especially the 4th version, a huge level up from the 3rd one, but its core still deficient[1] in some particular scenarious (see an intere

Lean is a great idea, especially the 4th version, a huge level up from the 3rd one, but its core still deficient[1] in some particular scenarious (see an interesting discussion[2] in the Rock (formerly Coq) issue tracker). Not sure if it might hinder the automation with the AI. [1] https://artagnon.com/logic/leancoq https://artagnon.com/logic/leancoq [2] https://github.com/rocq-prover/rocq/issues/10871 https://github.com/rocq-prover/rocq/issues/10871