Boolean Tipinden Ötesi

TypeScript ve çoğu programlama dilinde mantıksal ifadeler tek bir boolean tipine sahiptir ve true/false değerlerine çöker.

Lean’de 2 + 2 = 4 gibi ifadeler boolean yerine Prop (proposition) tipindedir ve kendileri bir değer olarak kalır.

Lean’de bir önerme aynı zamanda bir tiptir ve bu tipin elemanı olan kanıt (proof) önerme doğruluğunu ispatlar.

by rfl ve by decide gibi komutlar belirli biçimli önermeler ve hesaplanabilir ifadeler için Lean’e otomatik kanıt üretme imkânı sağlar.

Bir önermenin yanlışlığını ispatlamak için onun olumsuz önermesi (Not (…)=…) için kanıt sunmak gerekir.

Lean’de kanıtların içeriği önemsizdir (proof irrelevance); aynı önermeyi birden çok yolla ispat etmek mümkündür ve tüm kanıtlar eşit kabul edilir.

Lean’de ispat süreci tamamen tip denetimine dayanır; önerme ispatlandığında ilgili tipin değeri üretilmiş olur.

Kanıtsız bir önermeyi üretmek imkânsızdır; 2 + 2 = 5 gibi yanlış bir önermenin tipi içi boş bir tipe (never) benzer.