What is an example of a real functional language for you?

Haskell. But there are other examples of "pure functional programming". And the state of the art is dependently typed languages, which are essentially theorem provers but can be used to extract working code.

Like LEAN4 ?

I, too, am curious and keep checking back for a reply!