Proposizioni come tipi e valori in Lean

In TypeScript le espressioni logiche hanno tipo boolean con solo i valori true e false.

In Lean le proposizioni (ad esempio 2 + 2 = 4) hanno tipo Prop e non si riducono a boolean.

Per stabilire la verità di una proposizione in Lean occorre fornire una prova, cioè un valore del tipo della proposizione.

In Lean le proposizioni fungono anche da tipi e le loro prove sono valori di questi tipi, illustrando la corrispondenza Curry-Howard.

Una proposizione falsa corrisponde a un tipo senza valori; invece per dimostrare la falsità si fornisce una prova della sua negazione.

Gli strumenti by rfl e by decide facilitano la costruzione delle prove, ma la verifica finale avviene tramite typechecking del kernel di Lean.

In Lean tutti i proof di una stessa proposizione sono considerati equivalenti (proof irrelevance).

Dimostrare risultati matematici in Lean significa semplicemente creare e verificare valori di tipo corretto.