Yes. I'm impressed with Idris 2. I love how it uses Chez Scheme, my favorite scheme implementation. I contributed for a bit to getting Idris installation working on Apple Silicon Macs based on Racket's port of Chez Scheme, only to learn that I was working with Idris instructions that hadn't been updated.
Lean 4 is a better supported effort, with traction among mathematicians because of the math formalization goal.
I have more reasons to want to learn Lean 4. Peel away their syntax, and Lean 4 proofs are the word problem for typed trees with recursion. I find the reliance of AI on artificial neurons as arbitrary as so many advanced life forms on Earth sharing the same paltry code base for eyes, a nose, a mouth, and GI tracts. Just as many physicists see life as inevitable, in a billion runs of our simulation I'm sure AI would arise based on many foundations. Our AI fakes recursion effectively using many layers, but staring at the elementary particles that make up Lean proofs one sees a reification of thought itself, with recursion a native feature. I have to believe this would make a stronger foundation for AI.
I don't get that same rush looking at Idris. Using Lean 4 for general purpose programming? It must be good training.
I'm 53, impressed that you're still going at it at 69!