> No AI can code in Lean 4 reliably I wonder if this is due to the nature of the language. Lean 4 lets you redefine its syntax in ways that most other languag

> No AI can code in Lean 4 reliably I wonder if this is due to the nature of the language. Lean 4 lets you redefine its syntax in ways that most other languages do not allow[1], so effectively you are dealing with a recursive language, that could require a Touring complete token representation system. [1] https://leanprover-community.github.io/lean4-metaprogramming-book/main/05_syntax.html https://leanprover-community.github.io/lean4-metaprogramming... What other language lets you redefine the meaning of digits? The mix of syntax + macros + elaboration makes it really flexible, but hard to treat reliably. LLMs based on transformers are not Touring complete (nitpick: they are but only if you use arbitrary precision math, which is not the case in practical implementation https://arxiv.org/abs/1901.03429 https://arxiv.org/abs/1901.03429).