Proposisi sebagai Tipe dan Nilai di Lean

Dalam TypeScript, ekspresi logis selalu berjenis boolean dengan dua nilai true/false.

Di Lean, pernyataan logis berjenis Prop, bukan boolean.

Proposisi di Lean adalah nilai dan juga tipe; membuktikan proposisi berarti membuat nilai tipe itu.

Bukti seperti by rfl, by decide, dan two_add_two_eq_four menghasilkan nilai tipe proposisi.

Tanpa bukti, tipe proposisi seperti 2+2=5 tak memiliki nilai, mirip tipe never.

Negasi proposisi dibuktikan dengan membangun bukti untuk Not (2+2=5).

Lean menerapkan bukti tak relevan: semua bukti sejenis diperlakukan sama.

Verifikasi matematis di Lean adalah proses typechecking kernel.