Lean is a great idea, especially the 4th version, a huge level up from the 3rd o...

		xvilka 64 days ago \| parent \| context \| favorite \| on: Lean 4: How the theorem prover works and why it's ... 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 [2] https://github.com/rocq-prover/rocq/issues/10871

The issue was a fun read, thanks for sharing.