Matematikte Hayaletler Var

• 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

[GN⁺]

Hacker News görüşleri

• Bu aralar Lean gibi sistemleri (ya da doğrudan Lean’i) kullanarak haberleri veya kurgu dışı yazıları yeniden yazma fikri üzerinde düşünüyorum; yaklaşım, her ifadeyi kanıtlanması gereken bir teorem olarak ele almak ve kanıta alıntıları da dahil etmek. Örneğin, “onayladığım üç kaynak bunu olgu olarak söylüyorsa, bu bir olgudur” gibi bileşik bir kanıt olarak işlenebilir. Ayrıca tüm belgeyi, “kanıtlanmış” iddiaların öne çıkarılarak görülebileceği şekilde işaretlemek mümkün olabilir diye düşünüyorum. Mükemmel değil ama günümüz medyasının üstlendiği titizliği yeniden teknolojiyle ele alma girişimi gibi.
  • Doğal dildeki ifadeleri biçimselleştirmek, önünde sayısız engel bulunan bir alan. Bunun nedeni, gerçek dünyayla etkileşen kod yazmanın zor olmasına benzer: genelde kendiliğinden varsaydığımız kavramların tamamını (özdeşlik, zaman, nedensellik vb.) biçimsel sistem içinde ayrıntılı biçimde ele almak gerekiyor ki olgular birbirine bağlanabilsin ya da ifade edilebilsin. Yine de bu mesele gerçekten çok ilginç. OpenCog bu alanı sonuna kadar zorlayan bir projeydi; bilgi temsili ve akıl yürütme (KRR) diye ayrı bir araştırma alanı da var. IJCAI dergisi de bununla ilgili çalışmalarla dolu. Filozofların zaman/kip/olasılık gibi çeşitli akıl yürütmeleri biçimselleştirmek için geliştirdiği pek çok mantık da var ama ne yazık ki bunlar birbirleriyle kolayca birleşmiyor (yakın zamanda çözülmediyse tabii).
  • Haberlerde sahip olmamız gereken en önemli kanaatlerin çoğunun, mutlak önermeler koleksiyonu olarak kanıtlanabilecek şeyler olmadığını düşünüyorum. Bayes olasılığı gibi, akıl yürütme zincirlerini hesaplayan araçlar bana daha uygun geliyor. Bu tür sayısal tahmin araçları gördüm.
  • Üniversitede matematik aldıktan sonra kurgu dışı yazı yazma becerimin ciddi biçimde geliştiği deneyimim oldu. Eşim/sevgilim ve kız kardeşimin yazdığı denemeleri okuyup, sanki mantıksal bir kanıtı inceliyormuş gibi “burada C’nin B’den çıktığı söyleniyor ama B’nin A’dan nasıl çıktığı aslında eksik, o zaman C’nin A’dan çıktığını söyleyemezsin” türünden bir titizlik uyguluyordum. Bunu LLM gibi araçlarla bir programa dönüştürmek mümkün görünüyor ama halüsinasyonlar yüzünden sınırlar çok açık.
  • Dikkatli olmak gerekir; bu yaklaşım, özünde ne kadar radikal ya da saçma olursa olsun iddialara mantıksal nesnellik havasını kolayca verebilir. Modern mantığın kurucu isimlerinden Gottlob Frege’nin siyasi görüşleri buna dair bir uyarı olabilir ilgili bağlantı
  • Belirli bir konu hakkındaki tüm argüman yapısını harita gibi çizme fikri daha ilginç olabilir. Mesela “Tanrı var mı?” gibi büyük bir soruyla başlayıp, lehte ve aleyhte argümanları, bunlara itirazları ve karşı itirazları hiyerarşik biçimde açmak. Her iddiada “Platon böyle bir argüman ileri sürdü” gibi alıntılar, dayanak olmaktan çok tarihsel bağlam sağlamak için yer alır. Amaç kazananı belirlemek değil; aynı noktaların etrafında dönüp durmamak için bir argüman haritası kurmak.
• Sonunda birkaç apaçık doğrudan başlayan bir kanıt sözlüğü kurup, her tür kanıtın onun üstünde mantıksal olarak yığıldığı bir yapı mı oluşturuyoruz diye merak ediyorum. O zaman yeni kanıtlar, sadece mevcut kanıtların mantıksal birleşimleri olur. Keşke bunu Zachtronics tarzı bir oyuna dönüştürseler! Euclidea adlı oyun trigonometri alanında buna benzer bir his veriyor; mantık kulesi inşa etme fikri çok çekici. Acaba saf matematik gerçekten bu mu, saf matematik profesörleri bu mantık sözlüğünü genişletmekten haz mı alıyor? Bir de ünlü bir matematikçinin temel kanıtlar listesi hazırladığını hatırlıyor gibiyim; bunun kim/ne olduğunu ve ne dendiğini bilen varsa güzel olur. Muhtemelen bunlar aksiyomlardır.
  • Bununla ilgili bir oyun zaten var ama tam olarak aradığınız şey olmayabilir (ve tüm matematiği inşa etme oyunu da değil). Ben oynadım, oldukça eğlenceliydi. Bu yazıda geçen leanprover-community/nng4 tam olarak bu örnek.
  • “Bunu Zachtronics tarzı bir oyuna çevirsinler” kısmına cevap olarak, matematiğin kendisi zaten o oyun denebilir (biraz şaka tabii). Oyun sürümünün de gerçekten eğlenceli olacağını düşünüyorum. Saf matematik tam olarak böyle bir sistem. Lisans düzeyinde his bu yönde; makale araştırmasına çıkınca biraz farklılaşıyor. Oyun hissi istiyorsanız Dummit and Foote gibi soyut cebir kitaplarına da bakmanızı öneririm; kanıtlarda oyunvari bir keyif var. Ünlü kitapların çoğunda tıkanırsanız çevrimiçi çözümler de bulunabiliyor.
  • Belki de Öklid’in aksiyomlarından söz ediyorsunuzdur; nokta, doğru, düzlem, paralel doğru gibi kavramların tanımlandığı bir sistem. Düzlem yerine küre üzerinde bu sistem bozulur. Ya da Zermelo-Fraenkel küme kuramını (ZF/ZFC) kastediyor olabilirsiniz; modern matematik bunun üzerinde inşa edilir.
  • Bombe diye bir oyun da var; Mayın Tarlası’nın bir türevi. Hücreleri doğrudan açmak yerine, “hangi durumda bayrak koyulabilir” kuralları oluşturarak oynuyorsunuz. Seviye yükseldikçe kurallar lemmalar gibi birbirine zincirleniyor. Oyuncu becerisi arttıkça araç seti kısıtlarını gevşetip genelleme yapmak da mümkün oluyor oyun bağlantısı
  • Matematik özünde aksiyomlardan başlayıp sonuç çıkarmaktır. Elbette hepsi bu değil ama benim seviyemde anladığım kadarıyla böyle.
• Biraz ayrıntı takibi gibi olacak ama two_eq_two teoreminin bir fonksiyon gibi göründüğünü söylemek tuhaf; argümanı olmadığı için daha çok sabite benziyor (tabii sabitin de argümansız fonksiyon olduğunu biliyorum). Aşağıdaki gibi x_eq_x kullanıp bunu 2_eq_2 içinde fonksiyon gibi uygulamak daha ikna edici olurdu

  theorem x_eq_x (x:nat) : x = x := by
    rfl
  
  theorem 2_eq_2 : 2 = 2 := by
    exact (x_eq_x 2)
  

  Burada x_eq_x fonksiyon gibi görünüyor ve 2_eq_2 içinde de gerçekten öyle kullanılıyor.
  • Doğru bir nokta! Benim bunu öyle yapmamamın nedeni, Lean’in argüman işleme biçiminin (özellikle dependent types gibi kavramların — x verince x = x kanıtı döndürmesi) bana biraz yabancı gelmesi ve ayrı ele alınması gereken bir konu olması. Bir sonraki yazıda değineceğim.
• Lean öğrenirken zorlandığım nokta, rfl gibi tactic’lerin aşırı kapsayıcı olması ve eğitim materyallerinden bile tam olarak ne anlama geldiklerini çıkarmanın zor olması. Örneğin C dilinde bit düzeyine kadar durum değişimini izleyebilirsiniz ama Lean’de bir şeyler daha belirsiz geliyor. Bir de rewrite (rw) tactic sözdizimi doğal hissettirmiyor.
  • Coq’ta (artık Rocq) da tactic’lere alışmak hep zordu. Mesela “A = B” ve “P(A,A)” varken bunu “P(A,B)”ye dönüştürmek istiyorsunuz ama rewrite, açıklaması zor nedenlerle çalışmıyordu (muhtemelen aradaki yapı tanımları yüzünden). Buna karşılık Metamath ve set.mm veritabanı hiç tactic kullanmadan, tamamen somut çıkarımlarla kanıt yapmanızı istiyor (ax-mp gibi çıkarım kurallarıyla). Ama bu sefer de işe yarar yardımcı lemmaları ezberlemek gerektiğinden kolay olmuyor.
  • Agda’yı daha çok sevmemin sebeplerinden biri de bu. Agda’da neredeyse hiç tactic yok; Curry-Howard correspondence sayesinde fonksiyonel programlama dili yazar gibi doğrudan kanıt terimleri yazıyorsunuz. Ama soyutlama ve fonksiyon oluşturma konusunda tembel davranırsanız, ufacık şeyler bile saçma derecede zahmetli hale geliyor; yani disiplin önemli.
  • En azından Lean’de tactic tanımlarına “go to definition” ile gidip iç işleyişlerini görebilme avantajı var. Öğrenirken hacmi çok fazla geldiği için zorlayıcı ama sonuçta hepsini incelemek mümkün (temel tip kuramına inince sezgi biraz kayboluyor tabii). Bir de rewrite sözdiziminin doğal olmadığını söylemişsiniz; peki size doğal gelen bir rewrite sözdizimi nasıl olurdu, merak ettim.
  • İlginç gelen nokta, tactic’lerin tamamının kanıt çekirdeğinin (kernel) dışında, tamamen “kullanıcı seviyesi” kod olmasıydı. Küçük ve doğrulanmış çekirdeği değiştirmeden korumak istedikleri için mantıklı. Ama bu, tactic’ler sürüm yükseltmelerinde ya da değişikliklerde mevcut kanıtları bozabilir demek. Gerçekte bunun ne kadar sorun yarattığını merak ediyorum.
  • Benim beklentimin aksine Lean’de reflection ve rewrite’ın addition’dan daha temel olacağını sanıyordum. Lean sanki addition’ı hazır veriyor ama rfl ya da rewriteı her seferinde sizin yazmanız gerekiyor. Belki bunu otomatik yapan bir prelude benzeri sürüm vardır.
• Lean’de proof’ları etkileşimsiz, yani noninteractive biçimde okumanın bir yolu var mı diye merak ediyorum. Natural number game oynarken kanıtlar sadece rw [x] komutlarının sıralanışı gibi görünüyor ve okumak çok zor oluyor. Editörde her satırın durumuna bakabiliyorum ama sürekli tıklamak akışı bozuyor. Python’da da girinti olmasa ve akışı görmek için blok yapısına tıklamak gerekse aynı sorun olurdu. Benim deneyimim oyunun başındaki sınırlı komutlardan kaynaklanıyor olabilir ama gerçek, tam Lean ortamında bu akış daha iyi mi diye merak ediyorum.

  • Lean’de kanıtları noninteractive biçimde okumanın bir yolu var mı?
    Ben de bunu yakın zamanda merak edip araştırmıştım. lean-in-latex blogu tıklamadan, editör dışında da bu akışı takip etmeyi sağlayan bir yöntem sunuyor; ayrıca Lean topluluğunun buna nasıl yaklaştığını da görebilirsiniz.

  • Rocq’ta eskiden “mathematical proof language” diye bir şey vardı. Gerçek kullanım örneklerini bulmak zor ama aşağı yukarı şöyleydi

    Lemma foo:
      forall b: bool, b = true -> (if b then 0 else 1) = 0.
    proof.
      let b : bool.
      per cases on b.
        suppose it is true. thus thesis.
        suppose it is false. thus thesis.
      end cases.
    end proof.
    Qed.
    

    Bu yaklaşım, makaledeki “elle yazılmış kanıt” gibi okunmayı amaçlıyordu. Ama pek kullanılmadığı için kayboldu. Isabelle’in Isar proof dili de benzer ve hatta daha çok standart yaklaşım sayılır. Örnek:

    lemma "map f xs = map f ys ==> length xs = length ys"
    proof (induct ys arbitrary: xs)
      case Nil thus ?case by simp
    next
      case (Cons y ys) note Asm = Cons
      show ?case
      proof (cases xs)
        case Nil
        hence False using Asm(2) by simp
        thus ?thesis ..
      next
        case (Cons x xs’)
        with Asm(2) have "map f xs’ = map f ys" by simp
        from Asm(1)[OF this] ‘xs = x#xs’‘ show ?thesis by simp
      qed
    qed
    

    Burada genel mantıksal yapı ve ara sonuçlar açıkça yazılıyor; yalnızca ayrıntının önemli olmadığı yerlerde by ... ile tactic kısaltması kullanılıyor. Lean’de de benzeri var mı bilmiyorum ama en azından arama anahtar sözcüğü ya da Lean forumunda soru başlatmak için iyi bir referans olabilir.
  • Gerçekten çok iyi bir soru! Hâlâ acemiyim, o yüzden tamamen güvenmeyin ama hissettiklerimi paylaşayım. Lean’i birkaç aydır kullanıyorum ve anladığım kadarıyla proof kodu okumak program kodu okumaya benzemiyor; daha çok “tarama” gibi. Genel argüman yapısına, hangi tactic’lerin kullanıldığına, hangi lemma’ların çağrıldığına bakıyorsunuz. Gerçek Lean kod stilinde her yeni goal’da içeri girinti yapılır, goal bitince dışarı çıkılır; bu yüzden argümanın “şekli” önemli hale geliyor. Benim PR örneğim buna örnek olabilir. Tactic’lere alıştıkça intro görünce niceleyiciye girildiğini, constructor görünce goal’un bölündüğünü vb. ayırt etmeye başlıyorsunuz. Sonuçta tactic’ler kanıt ağacını (term tree) üreten makro/DSL’ler gibi. Ben proof koduna bakarken bunu ağaç üzerinde işlem yapmak gibi hissediyorum; parçaları bölmek, sıraları doldurmak vb. Yine de proof kodunun ortasındaki bir assertion’ın tam ne dediğini anlamak için hâlâ tıklamak gerekebiliyor. İyi fikir taşıyan kanıtlar, bir makalenin mantık akışı gibi net okunabiliyor. Bu yüzden niyetini aktarmak isteyen biri, okunaklı isimler, açık akış, küçük lemma’lara ayırma ve önce varsayımları yazıp sonra kısa proof kodlarıyla çözme yolunu seçiyor. Buna karşılık makine açısından zahmetli ama matematikçi için bariz olan kısımlar bazen “golfing” ile çok kısa yazılıyor. Golf tarzı, kodu kısaltırken genellikle insanın sezgisel olarak bildiği kısımları varsayıyor. Özetle, Lean’de okunan yapı örtük ama daha açık hale getirmenin yolları var; tactic’lerde ustalaştıkça tıklamadan da yapıyı daha iyi görmeye başlıyorsunuz. Sadece lemma adlarına bakarak bile genel akış anlaşılabiliyor ve sıra kolayca yeniden kurulabiliyor.
• İçerik gerçekten çok iyiydi; bunu kolay sindirilebilir biçimde anlatabilen insan çok az diye düşünüyorum. Uzmanların genelde atlayıp geçtiği küçük adımların hepsini göstermek işin sırrı.
  • Teşekkürler!
• Bu başlıkta Lean ile idris/coq/agda’nın geleceğine dair görüşleri duymak mümkün mü diye merak ediyorum. Bilgi temsili çalışmak istiyorum ama herhangi birine dalmadan önce topluluk büyüklüğü ve gelecekteki riskler beni düşündürüyor. Eskiden clojure core.logic’e zaman ayırıp çok düşük ilgi/küçük topluluk sorunundan canım yandığı için başlamakta zorlanıyorum.
  • Kendi deneyimime göre Lean ile Coq/Rocq, Idris ve Agda’dan çok daha yaygın kullanılıyor; kütüphane ve toplulukları da belirgin biçimde daha büyük. Rocq daha çok program doğrulama alanında kullanılıyor ama bence bu biraz tarihsel birikimden kaynaklanıyor; Lean de zamanla orayı yakalayabilir. Lean matematik teoremi kanıtlamada en yaygın seçenek gibi. Rocq’un bilinen projeleri arasında CompCert, CertiCoq, sel4 var; gerçek uçak yazılımı doğrulamasında kullanıldığı örnekler de mevcut (derli toplu bir proje listesi var). Lean tarafında mathlib (matematik kanıtları koleksiyonu), Fermat’ın Son Teoremi (FLT proof project), PFR gibi büyük projeler var. Idris ve Agda için gerçek “dünya” projeleri duymadım ama yanılıyor olabilirim. Tabii bunların hepsi C++ ya da JavaScript gibi dillerle kıyaslanınca çok küçük topluluklar. Ayrıca program doğrulama gerçekten çok yavaş ve sıkıcı bir iş. Yapay zeka gelişimi gibi temel bir değişim bir gün gelebilir ama yine de öğrendiğiniz beceriler boşa gitmez.
  • Bu alana “yatırım” yapma fikrine açıkçası çok sıcak bakmıyorum. Gerçekte matematikçilerin büyük çoğunluğu formalization ile çok ilgilenmiyor; elle yazılmış kanıtla bilgisayarın istediği katı sözdizimi arasında ciddi bir uçurum var. O yüzden buna daha çok öğrenme ve pratik yapma keyfiyle yaklaşmak lazım. Gelecek görünümünde Lean son dönemde en hareketli olanı gibi ama hepsinin köklü kullanıcı tabanları var; kesin konuşmak zor.
• Hiçbir teknik ya da hile olmadan, Lean’e rastgele bir şeyler atıp sadece kabul edip etmemesine bakarak ilginç keşifler çıkarmak mümkün mü diye merak ediyorum. Ya da bunu otomatik bir sistemle ya da LLM ile yapıp, karmaşık kanıtları/teorileri rastgele deneyip başarı durumuna bakmak mümkün mü? Sorum biraz tuhaf olabilir; Prolog’u bile ancak zar zor anlıyorum.
  • Ben certified programming işini profesyonel olarak yapan biri olarak, üretken yapay zeka ile formal methods’un mükemmel bir eşleşme olduğunu düşünüyorum. Hatta ileride LLM’lerin programcıların yerini alıp alamayacağı da, certified programming ve birleşimsel akıl yürütmeyle ne kadar iyi birleşebildiklerine bağlı olabilir.

    Rastgele şeyler atınca ilginç keşifler olur mu?
    Eski tarz yapay zeka, dama gibi durum uzayının küçük olduğu problemlerde iyidir. Satranç biraz daha zor, Go ise makine öğrenmesi olmadan geleneksel yapay zekâyla neredeyse imkânsız denecek kadar zor. Biçimsel dillerde ise olasılık uzayı, aranabilir durum sayısı, hayal edilenden çok daha büyük. Problemin yapısı yeterince netse SMT solver ile brute force yapılabiliyor. SMT solver’lar ile proof assistant’lar aslında formal methods’un ayrı kollarıydı ama artık birbirini tamamlıyorlar (bkz. Sledgehammer, Lean-SMT).
    LLM ya da otomatik sistemlerle rastgele kanıtlar/teoriler denetmek mümkün mü?
    Bu alan henüz tam ana akım araştırma değil ama epey çalışma yapılıyor. LLM patlamasından önce bile yıllardır büyük fonlar vardı. “Learning to Find Proofs and Theorems by Learning to Refine Search Strategies” gibi eski girişimler de var, DeepSeek-Prover gibi yeni çalışmalar da. Bunun nasıl eğitileceği ve gelecekte ne kadar ileri gideceği tamamen açık bir soru.
    Gerçek dünyadaki LLM’ler şu an Rocq ve Lean dillerinde hâlâ zayıf; üstelik yanlış bir yanıt geldiğinde onu düzeltmek çok acı veriyor. Yine de zamanla yapay zeka araçlarının seviyesi belirgin biçimde yükselecektir diye düşünüyorum.

  • Bu gerçekten çok canlı bir araştırma ve deney alanı!
    Lean topluluğu büyük ölçüde Zulip’te toplanıyor; Machine-Learning-for-Theorem-Proving kanalı içinde pek çok yararlı başlık bulabilirsiniz.
• Alphaproof sayesinde Lean’e ilk kez ilgi duyan biri olarak bu tanıtım yazısını çok beğendim. Lean’de şu anda neler yaptığınızı biraz anlatabilir misiniz?
  • Şimdilik sadece Lean ile matematik çalışıyorum. Özellikle Tao’nun Lean ders notlarını takip ediyorum; alıştırmalardaki boş sorry kısımlarını kendim doldurarak ilerliyorum (çözümlerim burada).
• Lean’de güvenilmeyen (sorry içeren) kanıtların ya da ek aksiyomların kullanılmasını otomatik olarak engelleyen bir doğrulama modu var mı diye merak ediyorum. Örneğin, “bu proof hiçbir şekilde sorry kullanmıyor” ya da “sabit bir aksiyom kümesinin kanıtlama gücüne dayanıyor” gibi şeyler doğrulanabiliyor mu?
  • Yazının ilerleyen kısmında geçen #print axioms some_theorem bunun örneği sayılmaz mı? Bununla, söz konusu kanıtın doğrudan ya da dolaylı olarak sorryye veya gözden geçirilmemiş aksiyomlara dayanıp dayanmadığını görebilirsiniz.
  • print axioms ile eklenmiş aksiyom olup olmadığını kontrol edebilirsiniz. Ayrıca warning ya da error olmadan derlenip derlenmediğine de bakabilirsiniz. SafeVerify yardımcı aracı, RL sistemlerinin keşfettiği bazı hileleri de yakalıyor.
  • Bunun makroyla da yapılabileceğine dair bilgi burada var.