[simonw]

Useful context: https://en.m.wikipedia.org/wiki/Lean_(proof_assistant) - "Lean is a proof assistant and a functional programming language. It is based on the calculus of constructions with inductive types. "