I'm 53, impressed that you're still going at it at 69!
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.
Everyone talks a good line about more powerful, expressive programming languages till they need to put in the work. Ten years effort to program like ten people the rest of your life? I'm 69 now, I can see how such an investment pays off.
I moved to OCaml. Studying their library source code is the best intro ever to functional programming, but I felt your "all the way" pull and switched to Haskell. (Monads make explicit what a C program is doing anyway. Explicit means the compiler can better help. What it comes down to is making programming feel like thinking about algebra. This is only an advantage if one is receptive to the experience.)
I'm about to commit to Lean 4 as "going all the way". Early in AI pair programming, I tested a dozen languages including these with a challenging parallel test project, and concluded that AI couldn't handle Lean 4. It keeps trying to write proofs, despite Lean's excellence as a general purpose programming language, better than Haskell. That would be like asking for help with Ruby, and AI assuming you want to write a web server.
I now pay $200 a month for Anthropic Max access to Claude Code Opus 4 (regularly hitting limits) having committed to Swift (C meets Ruby, again not just for macOS apps, same category error) so I could have first class access to macOS graphics for my 3-manifold topology research. Alas, you can only build so high a building with stone, I need the abstraction leverage of best-in-category functional languages.
It turns out that Opus 4 can program in Lean 4, which I find more beautiful than any of the dozens of languages I've tried over a lifetime. Even Scheme with parentheses removal done right, and with far more powerful abstractions.