Ah, my apologies, I wasn't particularly clear. The "best" I am referring to is only code generation into popularly used languages.

I'm currently using Lean myself, but Agda's probably going to win out longer term for me simply because it compiles to GHC Haskell.