- Lean, matematiği biçimsel olarak ifade edebilecek şekilde tasarlanmış bir programlama dilidir; matematikçilerin matematiksel teoremleri kod gibi ele almasını sağlar
- Kullanıcılar teorem, kanıt, aksiyom gibi öğeleri kod biçiminde yazar; kanıt süreci, tactic adlı bir komut kümesiyle ilerler
- Kanıt gerçekten tamamlanmamış olsa bile
sorry ile geçici olarak kapatılabilir, ancak bu TypeScript’teki any ile benzer bir sahte kanıttır
- Yanlış bir aksiyom eklenirse (ör.
2 = 3), mantıksal çelişki ve her önermeyi kanıtlayabilme riski doğar
- Lean yalnızca mantıksal olarak seçilen aksiyomlar ve kanıt sistemleri üzerinde sonuç ürettiğinden, matematiksel geçerliliği korumak büyük önem taşır
Lean: Matematiği Kodla İşlemek
- Lean, biçimsel matematiği yazmaya odaklanmış bir programlama dilidir
- Matematikçiler, Lean ile matematiği kod olarak ifade eder, teorem ve kanıtlarını yapısal hale getirerek iş birliği ve paylaşım sağlar
- İnsanoğlunun önemli bir matematik bilgisinin gelecekte kod biçiminde makine ile doğrulanabilir ve birleştirilebilir hâle geleceği bir geleceğe işaret eder
Lean’de Kanıtlamanın İlk Adımı
theorem two_eq_two : 2 = 2 := by sorry biçiminde Lean’de basit bir teorem bildirimi yapılabilir- Kanıt eksik olduğunda
sorry eklenebilir, ancak bu sadece bir geçici çözümdür ve gerçek bir kanıt değildir
sorry, Lean’in kanıt doğrulamasını geçmesine olanak sağlar, fakat mantıksal açıdan güvenilir değildir
- Tam bir kanıt için
rfl (reflexivity) gibi bir tactic kullanılarak, 2 = 2 gibi apaçık eşitlikler kanıtlanır
- Önceden ispatlanmış içerikler,
exact gibi komutlarla diğer teoremlerde yeniden kullanılabilir; bu da modülerliği vurgular
Aksiyom ve Çelişki: Matematikte Hayalet Görünüm
axiom math_is_haunted : 2 = 3 gibi bir aksiyom eklenirse Lean bunu doğru sayar- Bu aksiyom kanıt sürecinde kullanılabilir; böylece matematiksel olarak anlamsız görünen sonuçlar (ör.
2 + 2 = 6) bile kanıtlanabilir hale gelir
rewrite taktiğiyle 2yi 3e dönüştürüp rfl ile eşitlik kanıtlama adımı tamamlanabilir- Yanlış aksiyomlardan doğan çelişki durumunda Lean’de de her önermenin kanıtlanabildiği bir durum (mantıksal çöküş) ortaya çıkar
- Nitekim 20. yüzyıl başındaki Russell paradoksu gibi aksiyomatik sistem içi çelişkiler, matematiğin temel sorgulamasına yol açmıştı
- Lean bu şekilde aksiyom seçiminin, bir mantık sisteminin geçerliliğini korumada belirleyici rol oynadığını açıkça gösterir
Kanıt Denetleyicisi (Proof Checker) Olarak Lean
- Aksiyomlar doğru seçilip Lean mantıksal olarak tutarlıysa, teorik olarak güvenilir sonuçlar üretilir
- Basit bir eşitlikten
Fermat’ın Son Teoremi gibi çok karmaşık teoremlere kadar hepsi aynı ilkeyle doğrulanır
- Büyük teoremler, alt yapılar ve teoremlerin tekrar edilen kanıtlarıyla tamamen bir ağaç gibi inşa edilir
- Örnek olarak, Fermat's Last Theorem’in Lean’de biçimselleştirildiği büyük bir proje sürmektedir; sonuçta
sorry içermeyen son derece resmi bir kanıt sisteminin tamamlanması beklenmektedir
Lean’i Öğrenmenin Zevki
- Lean ile kanıt yapmak, kodlama ile matematiğin yaratıcı birleşimidir
- Başta basit bir önerme ispatlamayla başlayan süreç, zamanla giderek daha karmaşık ve derin matematiği katı kurallarla inşa etmenin keyifli bir yolculuğu olur
- Resmi dersler ve topluluk kaynakları (ör. Natural Numbers Game, Mathematics in Lean gibi) giriş için uygundur
- Lean’i kullanarak mantığı doğrudan biçimlendirdiğinizde, keskin fikirlerin ve mantıksal argümanların estetiğini yeniden keşfedebilirsiniz
- Nedensiz gibi dursa da, belirli bir kesim için Lean’in özel bir eğlence kaynağı olduğu sonucuna varılır
Henüz yorum yok.