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.