Hacker News Reader

Lean the theorem proving language?

Indeed, though I have no quote or link for this "claim".

Well, functional programming is very natural for theorem provers, especially those based on the Curry-Howard correspondence.