Matematikçilerin Lean Teorem İspatlayıcısı Hakkında Bilmesi Gerekenler: Güvenilirlik ve Yapay Zeka

Terence Tao'nun blogunda Thomas Hales tarafından kaleme alınan bu yazı, yapay zeka yardımıyla biçimlendirilmiş bir konuk makaledir. Değerlendirmenin merkezinde; matematiğin bilim ve medeniyete sunduğu eşsiz güvenilirlik ile içsel tutarlılığı yer almaktadır.

Matematiğin Biçimselleştirilmesi#

Biçimsel (formal) ispat; temel mantık kuralları ve aksiyomatik temeller düzeyinde bilgisayar yazılımlarınca eksiksiz şekilde denetlenen matematiksel kanıttır. Teorik olarak elle yapılabilmesi mümkün olsa da içerdiği devasa işlem adımları nedeniyle süreç genellikle özel yazılımlarla yürütülür. Bu sistemler literatürde ispat asistanları (proof assistants), teorem ispatlayıcılar (theorem provers) veya etkileşimli teorem ispatlayıcılar (interactive theorem provers) olarak adlandırılır.

Bugüne kadar başarıyla biçimselleştirilen başlıca teoremler şunlardır:

• Dört Renk Teoremi (Four-color theorem)
• Feit-Thompson (Tek Dereceli) Teoremi (Odd-order theorem)
• Kepler Varsayımı (Kepler conjecture)
• Küre Tersyüzü (Sphere eversion)
• 8 ve 24 Boyutta Küre Paketleme Problemi
• Navier-Stokes Zorlamalı Patlama (Forced blowup)
• Fermat'nın Son Teoremi (Fermat's Last Theorem)

Son üç projenin bu yıl tamamlanması, biçimsel ispat yöntemlerinin potansiyelini tüm bilim dünyasında geniş bir farkındalığa ulaştırmıştır.

Yıllar içinde geliştirilen öne çıkan 7 ispat asistanı şunlardır:

• Automath
• HOL Light
• Isabelle
• Coq (geçen yıl Rocq olarak yeniden adlandırıldı)
• Metamath
• Mizar
• Lean

Freek Wiedijk’in editörlüğünü yaptığı "The Seventeen Provers of the World" adlı kitap, bu kanıtlayıcıları karekök 2'nin irrasyonelliği ispatı üzerinden kıyaslamaktadır. Günümüzde matematikçiler arasında en popüler olan sistem ise Lean'dir. 2013'te Microsoft bünyesinde Leo de Moura tarafından geliştirilen Lean, de Moura'nın girişimiyle açık kaynak kodlu hale getirilmiştir. Kevin Hartnett'in "The Proof in the Code" kitabına göre, Carnegie Mellon bünyesindeki yeni NSF enstitüsü ICARM'ın yöneticisi Jeremy Avigad, Lean'in ilk kullanıcısı olmuştur. Avigad'ın 2015'teki seminerinin ardından, 2017 yılında Mario Carneiro ve Johannes Hölzl çekirdek kütüphaneden yola çıkarak bağımsız bir matematik kütüphanesi olan mathlib'i başlatmıştır.

mathlib Ekosisteminin Büyüklüğü:

• Yaklaşık 300.000 teorem
• 100.000'den fazla tanım
• 2,5 milyon satır kod
• 700'ü aşkın bağımsız katkıcı

Kütüphanedeki herhangi bir teorem, tıpkı modern yazılım mimarisinde bir fonksiyon çağrısı gibi doğrudan referans verilebilir. Örneğin Cauchy-Schwarz eşitsizliğini kullanan bir kanıt, teorem kütüphaneden içe aktarılarak (import) sıfırdan kanıt yazma zahmetinden kurtulur.

Otomatik Biçimselleştirme Pratik Bir Gerçekliktir#

Geçmişte kağıt üzerindeki ispatların biçimsel koda aktarılması yoğun insan emeği gerektiriyordu. Nitekim 3 boyutlu küre paketlemelerine dair Kepler varsayımının biçimsel ispatı yaklaşık 20 insan-yılı iş gücü almıştı. Günümüzde yapay zeka destekli otomatik biçimselleştirme (autoformalization), bu çeviri sürecini hızlandırarak pratik bir gerçekliğe dönüştürmüştür.

Yazılım Geliştirme ve Öğrenme Çıkarımları#

• En Uç Seviye Tip Güvenliği: Lean, derleyicinin sadece sözdizimini değil, kodun mantıksal kesinliğini doğruladığı nihai statik tip denetimidir.
• Modülerlik ve Açık Kaynak Kültürü: Mathlib; sürüm kontrolü, bağımlılık yönetimi ve modüler kod tasarımıyla devasa yazılım projelerinin nasıl yönetileceğine harika bir örnektir.
• Yapay Zeka Halüsinasyonuna Karşı Deterministik Kalkan: LLM'lerin ürettiği kod ve mantık iddiaları, Lean gibi deterministik bir doğrulayıcı ile test edildiğinde sıfır hata toleranslı akıl yürütme elde edilir.