Ud over Booleske Værdier

I de fleste programmeringssprog har logiske udtryk typen boolean med kun to værdier: true eller false.

I Lean har udsagnet `2 + 2 = 4` typen Prop i stedet for boolean.

Propositioner i Lean er både værdier og typer – fx er `2 + 2 = 4` en type, som beviser kan have.

At bevise en proposition i Lean svarer til at konstruere en værdi af dens type.

By rfl kan automatisk bevise lighedspropositioner som `2 = 2` og `2 + 2 = 4`.

By decide kan bevise enhver beregnelig udsagnstype, fx `Not (2 + 2 = 5)`.

En proposition anses for falsk, hvis man kan konstruere en bevisværdi for dens negation.

Bevisirrelevans betyder, at alle beviser for samme proposition betragtes som ligeværdige.

Lean indlejrer logik i typesystemet: sandhed svarer til succesfuld typetjek.