Para Além dos Booleanos

Em TypeScript expressões lógicas têm tipo boolean e colapsam imediatamente em true ou false.

Em Lean expressões como `2 + 2 = 4` têm tipo Prop e não se avaliam automaticamente.

Em Lean proposições são valores e também tipos, e provar uma proposição significa fornecer um valor desse tipo.

Provas em Lean são valores construídos com táticas como `by rfl` e `by decide`, e são verificadas pelo sistema de tipos.

A negação de uma proposição em Lean é uma Prop distinta e requer prova própria para ser considerada verdadeira.

Em Lean diferentes provas da mesma proposição são consideradas irrelevantes e equivalentes.

Proposições impossíveis de provar (como `2 + 2 = 5`) são tipos sem valores possíveis, semelhante ao tipo never em TypeScript.