I'm running tests for an involved math research project, and to my great surprise Lean 4 << Haskell << OCaml in execution times (so far).

I love Lean 4, but good luck getting help with it from AI. Today's project-in-progress is digesting their reference manual to fit well within a 200K context window. We'll see if that helps.