This is an unbelievably good explanation of some very difficult concepts. I think the Lean documentation should start with an enormous link to this post.

Highly recommended to anyone interested in Lean who isn't already an expert.

The name "bool expression" is rather unfortunate, since it is usually reserved for "an expression of type Bool". What is discribed here is really propositions, i.e. "Prop".

Prop is fundamentally different from Bool in Lean and all the language I know. For lean in particular, Prop is defined as a complete lattice, yet Bool is only inhabited by True and False (ignoring incomputable etc). More intuitively, Bool require all the true (or false) statements to be collapsed into a single value true (or false); yet for Prop, provable statements are not necessarily equal to each other.

But I really enjoyed the analogy between expressions that returns bool in other languages and leans prop, seem like a great starting point for people.