Neden Sadece Lean Kullanmıyoruz?

 (lawrencecpaulson.github.io)
1 puan yazan GN⁺ 2026-04-29 | 1 yorum | WhatsApp'ta paylaş
  • Matematiğin biçimselleştirilmesinin tarihi Lean ile başlamadı; yaklaşık 60 yıl önceye uzanan farklı sistem soyları, temel teknikleri ve başarıları zaten biriktirmişti
  • 1968 tarihli AUTOMATH, LCF ailesi, HOL, Rocq, ACL2 ve Mizar gibi araçlar, reel analizden asal sayı teoremine, dört renk teoreminden Kepler varsayımına kadar geniş kapsamlı biçimselleştirmeler ortaya koydu
  • Lean, büyük bir kütüphane ve canlı bir topluluk sayesinde modern matematik tanımlarını hızla biriktirdi; ancak propositions as types ya da bağımlı tipler, proof assistant için tek yol değil
  • Isabelle, güçlü otomasyon, yüksek okunabilirlik ve bağımlı tiplerden kaçınmayı avantaj olarak öne çıkarırken, proof object olmadan da çekirdeğin soyutlama bariyeri üzerinden kanıt denetimi kuran LCF geleneğini sürdürüyor
  • Yapay zekanın yapılandırılmış kanıtları düzenleyip başka sistemlere çevirme yönündeki akışın da eklenmesiyle, tek bir aracı mutlak ölçüt olarak görme baskısı gelecekte daha da azalabilir

İlk sistemler ve diğer soylar

  • AUTOMATH

    • AUTOMATH, 1968'de matematik biçimselleştirmesi için gereken unsurların çoğunu zaten içeriyordu
    • 1977'de Jutting, AUTOMATH ile Landau'nun Foundations of Analysis eserini biçimselleştirdi ve saf mantıktan başlayıp karmaşık sayıların inşasına kadar ilerledi
    • Eşdeğerlik sınıfları ve rasyonel sayı kümelerini kullandı, reel doğrunun Dedekind tamlığını da biçimsel olarak kanıtladı
    • Bu başarı 20 yıl boyunca tekrar edilemedi; reel sayı biçimselleştirmeleri ancak 1990'ların ortasında John Harrison'ın HOL Light'ında ve Jacques Fleuriot'nun Isabelle/HOL'unda yeniden ortaya çıktı
    • Gösterim çok elverişsizdi ve hiç otomasyon olmadığından kanıtlar uzun ve okunması zordu
    • Buna rağmen eşdeğerlik sınıflarını ele almada Rocq'dan daha iyi olduğu düşünülüyor; Rocq kullanıcılarının yaşadığı setoid hell'in aksine Jutting, eşdeğerlik sınıflarını sakin biçimde biçimselleştirdi

  • Boyer ve Moore

LCF sonrası akış

  • Edinburgh LCF programlama dili teorisine odaklanmıştı; ancak proof assistant'ın meta dili olarak işlevsel bir dil kullanma fikri geniş ölçüde yayıldı
  • Cambridge, INRIA, Cornell gibi birçok grup, ML kullanarak ilk HOL, Coq (bugünkü Rocq) ve Nuprl gibi araçları geliştirdi
  • HOL grubu donanım doğrulamaya odaklanmıştı; ancak kayan noktalı donanım doğrulaması nedeniyle reel analize ihtiyaç doğdu
  • John Harrison, Cauchy integral formülü üzerinden asal sayı teoremi gibi ciddi matematik sonuçlarını HOL ailesinde kanıtladı
  • 100 theorems listesinden mümkün olduğunca çoğunu doğrulama hedefi altında HOL Light sık sık en üst sıralarda yer aldı
  • 2014'e kadar bu ailedeki sistemler birçok ileri düzey teoremi biçimselleştirmişti
  • Bu teoremlerin kanıtları genellikle uzun ve karmaşıktı; biçimselleştirme çalışmaları da çok büyük ölçekliydi ve teoremlerde kalmış şüpheleri azaltmada kritik rol oynadı
Reklam

Lean topluluğunun yükselişi

  • Matematikçiler, önceki biçimselleştirme başarılarının Grothendieck şemaları ya da perfectoid spaces gibi ana akım modern matematiğin incelikli yapılarıyla tam anlamıyla ilgilenemediğini düşünüyordu
  • Tom Hales bu tür tanımları kütüphane olarak üst üste inşa etme yönünü seçti; kanıtlardan çok tanımların birikimine odaklandı ve Lean'ı tercih etti
  • Bu yönelimi Big Proof programında sundu; benzer fikirler de orada tartışıldı
  • Kevin Buzzard bunu dinledikten sonra eğitimde Lean kullanmayı denemeye karar verdi ve ardından yayılım hızlandı
  • Lean topluluğunun önemli bir dönüm noktası olarak, Rocq'ya uzun süre hakim olan konstrüktif kanıt saplantısından uzaklaşması gösteriliyor
  • Sezgicilik, Russell paradoksundan sonra ortaya çıktı ve reel sayı kavramı için de belirli sonuçlar doğurdu
  • Martin-Löf type theory açıkça sezgici bir biçimcilik olsa da, Rocq'nun bu kadar basit görülmemesi gerektiği belirtiliyor
  • Buna rağmen Rocq ile ilgili makalelerde, konstrüktif kanıtlar ilgisiz ya da anlamsız oldukları yerlerde bile tekrar tekrar ortaya çıktı; bu eğilimin Rocq'nun matematikte uygulanmasını zorlaştırarak alanı Lean'a bıraktığı düşünülüyor

propositions as types ve LCF arasındaki fark

  • Propositions as types, mantık sembolleri ∀, ∃, →, ∧, ∨ ile tip kurucuları Π, Σ, →, ×, + arasındaki ikiliktir
  • Bu çerçeve güzel ve kuramsal olarak üretkendir, ancak tek yol değildir
  • Bir proof assistant'ı, propositions as types ilkesiyle kanıt denetleyen yazılım olarak sınırlarsak, son yarım yüzyıllık araştırmanın büyük kısmı tanımın dışına itilir
  • O zaman geriye yalnızca Rocq, Lean ve Agda kalır
  • Hatta AUTOMATH bile propositions as types örneği değildir; Π ve →'ya benzeyen ögeler olsa da mantığı genel mantık ders kitaplarında olduğu gibi aksiyomlarla kurar
  • de Bruijn, 50 yıl önce bile tiplerle önermelerin ayrılması gerektiğini düşünüyordu
  • Örneğin bölme işlemi üç argüman almalıdır ve (x/y)'nin değeri (y \ne 0) kanıtına bağlı olacağından proof irrelevance gerekir
  • LCF yaklaşımının propositions as types ile aynı olduğu düşüncesi de açıkça yanlış bulunuyor
  • Rocq ve Lean'da, önermelerin sort'u olan Prop bulunur; burada aynı önermeye ait tüm proof object'ler aynı değer sayılır ve böylece proof irrelevance sağlanır
  • Ancak bu, devasa proof object'lerin ortadan kalktığı anlamına gelmez; gerçek sistemlerde hâlâ varlıklarını sürdürürler
  • Robin Milner'ın temel keşfi, LCF'de proof object'in kendisine ihtiyaç olmamasıydı
  • Kanıt çekirdeği, ML'in soyut veri tipi içine yerleştirilip çıkarım kuralları kurucu olarak tanımlanırsa, kanıtlar dinamik olarak denetlenebilir
  • ML'in abstraction barrier yapısı sayesinde hile yapılamayacağı kabul edilir
  • Hiçbir şeye işaret etmeyen devasa terimlerin onlarca MB yer kaplaması, özellikle RAMmageddon çağında daha da irrasyonel görünüyor
  • Bu gereksiz terimleri daha zarif hale getirmeye yönelik araştırmaların sürmesi de eleştiriliyor

Isabelle'i seçmek için nedenler

  • Meslektaşlarınız Lean kullanıyorsa, ekibin uzmanlığı Lean'daysa ve gerekli öncül kütüphaneler Lean'da bulunuyorsa, Lean kullanmak doğal seçimdir
  • Yine de serbestçe seçim yapılabiliyorsa, Isabelle'i değerlendirmek için açık nedenler vardır

  • Otomasyon

    • Avantaj olarak en güçlü otomasyonu gösteriyor; gündelik “hammer” araçlarıyla karşılaştırıldığında bile sledgehammer ile boy ölçüşebilecek pek az şey olduğunu söylüyor
    • Bilgisayarlı cebir tarafının da ayrıca ele alınması gerektiğini belirtiyor

  • Okunabilirlik

    Reklam

  • Bağımlı tiplerden kaçınma

    • Bağımlı tipler olmadığı için, universe level ve yeni başlayanları zorlayan çeşitli tuhaflıklar da önleniyor
    • Lean'ın mathlib'inde ve Rocq'nun SSReflect ile Mathematical Components ekosisteminde de bağımlı tip kullanımının önerilmediğini belirtiyor
    • Bağımlı tiplerin temel zorluğu, doğru biçimde uygulanırlarsa tip denetiminin kendisinin karar verilemez hale gelmesidir
    • Bunun nedeni eşitlik kararının karar verilemez olmasıdır; başlangıçta bunun doğal karşılandığını söylüyor
    • Yaklaşık 1990'dan itibaren ise tip denetimini karar verilebilir kılmak için eşitliğin definitional/intensional equality düzeyine indirilmesi yönünde bir uzlaşma oluştu
    • Bunun sonucu olarak (T(N+1)) ile (T(1+N)) farklı tipler haline geldi
    • Bu kısıtlar gerçek kanıtları da etkiliyor ve definitional equality denetimi bile hâlâ hesaplama yükü taşıyor

Bağımlı tipler olmadan da mümkün olan modern matematik

  • 2017 itibarıyla, Isabelle'in ne tür matematikleri kaldırabileceği konusunda çok daha temkinli düşündüğünü belirtiyor
  • O dönemde şu konuları ele almak için bağımlı tiplerin zorunlu olduğu kolayca düşünülebilirdi
  • Ancak Alexandria ile ilgili çalışmalar sayesinde çok şey öğrenildiği ve kilit noktanın her şeyi tiplere itmemek olduğu sonucuna vardığı belirtiliyor

Gelecek yönelim ve yapay zeka

  • Lean birçok şeyi doğru yapıyor ve iç içe geçmiş kanıt bloklarını da desteklediği için potansiyel olarak yeterince okunabilir bir kanıt dili olabilir
  • Artık Lean topluluğunun bu özellikleri gerçekten kullanması gerekiyor; Isabelle kullanıcılarının ise zaten büyük ölçüde bunu yaptığı belirtiliyor
  • Bilgisayarın denetleyebildiği proof object'lerden çok, insanların gerçekten okuyabildiği kanıt metninin şeffaflığı daha önemlidir
  • Yapay zekanın yükselişi bu farkı daha da görünür kılıyor
  • Yapay zekanın ürettiği kanıtlar çoğu zaman dağınık oluyor; ancak sledgehammer ile düzenlenmeleri kolay ve yapı iyi kurulmuşsa ayrıntı fazla olsa bile okunabiliyorlar
  • Bu sayede ilerleyişin akışını görmek ve daha basit bir biçime indirgemek kolaylaşıyor
  • Son dönemde, dil modellerinin doğrudan sledgehammer çağırdığı araştırmalar da çıktı
  • Yapay zeka, okunabilir ve yapılandırılmış kanıtları bir proof assistant'tan diğerine çevirme işini de kolayca yapabilir
  • Böyle olursa, hangi sistemi seçmek gerektiğine dair baskı da azalır

Mizar eksikliğinin giderilmesi

  • Matematik biçimselleştirmesinin tarihi, Mizar ve onun devasa matematik kütüphanesi olmadan tamamlanmış sayılmaz
  • Isabelle'in Isar dili de Mizar'dan büyük ölçüde etkilenmiştir
  • Mizar'ın atlanmış olmasını ayrıca düzeltiyor ve bir sonraki yazıda Mizar'ı ele alacağını belirtiyor

İlgili okumalar

1 yorum

 
GN⁺ 2026-04-29
Hacker News görüşleri

  • HN okurlarının çoğu matematikçiden çok programcıya daha yakın olduğu için, Lean’e matematiksel kanıttan ziyade programlama açısından bakmanın daha pratik olduğunu düşünüyorum
    Lean’i fonksiyonel programlama perspektifiyle ele alan kitaplardan https://leanprover.github.io/functional_programming_in_lean/ oldukça iyi
    Ben de Lean öğreniyorum, o yüzden acemiye özgü biraz pembe bir bakışım olabilir; ama son dönemde lean-zip örneğinde olduğu gibi gerçek sıkıştırma/açma algoritmaları gibi sıradan programcı kodlarını yazıp kanıtlayabilmeyi hedefliyorum
    https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...

    • Bu kitabı okurken Lean ile temel bir bilgisayar cebiri sadeleştiricisi üzerinde biraz oynadım
      https://github.com/dharmatech/symbolism.lean
      C# kodunun bir portu ve Lean’in ifade gücü şaşırtıcı derecede yüksek
    • Böyle bir kullanım için Dafny de benzer bir seçenek sayılmaz mı diye düşünüyorum
      Bir ara biraz gündem olmuştu, ama son dönemde bu alanı yakından takip etmedim
    • 1990’larda yazılım doğruluk kanıtı denemeleri yapılan bir örneği hatırlıyorum; nihai kanıt açıklamaları kısmında gerçek yazılımdan daha fazla hata çıkmıştı diye hatırlıyorum
      Ayrıca iki engel daha görüyorum. Birincisi, yazılımın ne yapması gerektiğini bilmek başlı başına zor ve kullanıcının yapmak istediği şeyle müşterinin para ödediği şey de her zaman aynı olmuyor
      İkincisi, birçok geliştiricinin iş kalitesi o kadar düşük ki Java gibi dillerden daha iyi hakikat dili kullanmalarını beklemek zor
      Ama ikincisi, gereken özeni gösteren AI sistemleriyle yer değiştirdikçe ortadan kalkabilir; o zaman tablo değişebilir
    • Fonksiyonel olmayan programlama için durum ne diye düşünüyorum
      Fonksiyonel programlamanın da, çoğu programcı için çok da ilgili olmayan ve çoktan geride bırakılmış matematik kadar alakasız kaldığını düşünüyorum

  • Yazarın Lean’i epey yanlış anladığı anlaşılıyor; alanı iyi bilen biri gibi göründüğü için bu daha da şaşırtıcı
    Lean’in kanıt nesnelerini olduğu gibi koruduğunu ve sonunda tüm tanımların açıldığı devasa bir kanıt nesnesini denetlediğini sanıyor gibi, ama bu gerçekle pek örtüşmüyor
    Lean, yazarın LCF’nin avantajı diye övdüğü optimizasyonu fiilen neredeyse birebir uyguluyor. Bir benzetmeyle, kanıtı tahtayı silerek ilerletmek gibi
    Lean4’te def yerine theorem ile yazarsanız, o kanıt nesnesi artık kullanılmaz; bu sadece bir optimizasyon değil, dilin temel özelliğidir. theorem opaque’tir
    Kanıt terimi ortada kalsa bile bunun tek nedeni etkileşimli modda kullanıcıya gösterilebilmesidir; kernel ise o kanıt nesnesinin ne olduğuyla ilgilenmez bile

    • Bu, uygulamadan çok kavramsal bir fark gibi
      LCF’de kanıt ve terim farklı şeylerdir ve bence aslında öyle olması gerekir. Bu tür Curry-Howard tarzı karışıklık gereksiz; ama birçok kişi bilgisayarla matematik yapmanın tek yolunun bu olduğunu sanıyor
      İsterseniz LCF’de de kanıtları saklayıp kullanabilirsiniz, Lean’de de isterseniz optimizasyonla ortadan kaldırabilirsiniz
    • Bağımlı tip teorisinde kanıt nesnesi, yalnızca belli bir tipi dolduran terimin kendisi olduğuna göre, Lean uygulamasının böyle terimler üretmeden kanıt inşa edebilmesi mi kastediliyor diye merak ediyorum
    • Doğru gibi görünüyor
      Soyut tip yaklaşımı biraz bellek kazandırabilir ama bu yalnızca sabit katsayı düzeyinde bir farktır, asimptotik bir iyileşme değildir
      Lean’in onlarca MB harcadığından şikâyet etmek 1980’ler ve 90’larda önemli olabilirdi ama bugün o kadar belirleyici bir avantaj olmayabilir

  • Lean’in fonksiyonel programlama için iyi olduğunu sık duyuyorum ama Agda’dan gelince biraz kaba bir geriye gidiş gibi hissettiriyor
    tactic’lerin de iyi olduğu söyleniyor ama benim deneyimimde Coq tactic’leri daha güçlü ve kullanımı daha kolaydı
    Bu tamamen ilk izlenim yanlılığı da olabilir, ama şimdiye kadar Lean’in gücü bir şeyi herkesten iyi yapmasından çok, genel olarak yeterince iyi olması ve topluluğunun büyük olmasında gibi görünüyor
    Neden çekici olduğunu anlıyorum ama bunun bedeli olarak biraz güzellik ve güç kaybolmuş gibi, o da üzücü

    • Sonuçta bu bir tür ağ etkisi meselesi
      Ama bu tür etkiler o anda kalıcıymış gibi görünse de gerçekte sanıldığından kısa sürebilir. Sadece bu önemli olsaydı, Perl bugün hâlâ devlerden biri olurdu
      Lean özelinde özellikle önce büyük bir kütüphane edinmiş olması önemli. Perl için CPAN neyse o gibi
      Ama ölçekleme yasalarına bakınca, çoğu kullanıcı için büyük bir kütüphanenin değeri muhtemelen boyutunun logaritması kadar artar
      https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...
      Başta bu fark kapatılamaz gibi görünür ama bir noktadan sonra sırf ölçeği yakalamak değil, kullanılabilirlik daha önemli hale gelir
      Üstelik matematik kütüphanesi port etmek LLM’lere çok uygun bir iş. Kaynak doğrulanmış, hedef doğrulanabilir ve akıl yürütme yolu da büyük ölçüde taşınabilir
      Tersinden bakarsanız, LLM’ler sayesinde küçük platformlarda çalışmanın eşiği de beklenenden daha düşüyor. O taraftaki kütüphaneyi kendi platformuma taşıyabiliyorsam, kendi kanıtımı da oraya taşıyabilme ihtimalim yüksektir
    • Hatta bu daha çok topluluğun sonunda olgunlaşıp gerçek işler yapmaya başladığını gösteriyor gibi
      Mükemmel araç asıl mesele değil; yeterince iyi bir araçla işi bitirmek daha önemli
    • Agda kanıt denetleyicisi olarak daha iyi olabilir ama yazılım geliştirmek için pratik bir seçenek olduğunu düşünmüyorum
      Lean, gerçekten Haskell’in halefi olabilecek kadar yazılım geliştirmeye uygun bir fonksiyonel dil haline gelme potansiyeli taşıyor gibi görünüyor
    • Agda’yı biraz, Lean’i ondan daha fazla kullandım; matematiksel kanıtlardan çok genel fonksiyonel programlar yazmak Lean’de çok daha kolaydı
      Fark büyük ölçüde araç desteğinden geliyordu sanırım. Agda belgeleri zayıf, sistemi kurup çalıştırmak zahmetli ve fiilen Emacs kullanmanızı güçlü biçimde dayatıyor
      Buna karşılık Lean’in kendi belgelerinde cat yardımcı programının nasıl yazılacağı bile var ve genel olarak çok daha modern bir tooling deneyimi sunuyor
    • Agda’nın fonksiyonel programlama tarafında tam olarak neyin daha iyi olduğunu merak ediyorum
      Genelde övgüyü daha çok dependent pattern matching konusunda duyuyorum; o noktada Lean bana oldukça zayıf geliyor
      Yine de genel FP’de de Agda’yı daha dostça buluyorsanız, hangi açılardan olduğunu duymak isterim

  • Isabelle/HOL’un dili kendi başına fena değil ama tooling tarafında, masaüstü merkezli yaklaşımını bir yana bıraksak bile, derin kusurlar var
    Dil Lean’den mutlaka daha iyi değil, sadece farklı ve bağımlı tiplere yönelik bazı eleştirilere katılıyorum
    Sonuçta iki dil de farklı ödünleşimler yapmış ve bu seçimler onları kendi alanlarında epey verimli araçlara dönüştürmüş gibi. Kanıt alanı başlı başına geniş; her paradigmanın güçlü ve zayıf yanları var ve Lean bunların başka bir kısmında uzmanlaşmış durumda
    Sledgehammer iyi ama Lean’de de benzeri bir şeyin ortaya çıkması zaman meselesi gibi
    Keşif aşamasında yararlı olabilir ama çok kaynak tüketiyor; kanıtları kısaltıyor olsa da açık kodda yarı büyülü by sledgehammer yerine kanıtın tüm adımlarının doğrudan görünmesini tercih ederim
    Buna karşılık Isabelle’in kendisini geliştirmek, Lean’e kıyasla çok daha acı verici; özellikle de geliştiricilerle iletişim kurma kısmı
    E-posta listesinde hata yoktur, sadece beklenmedik davranış vardır tarzı tutum çocukça ve profesyonellikten uzak görünüyordu
    Ayrıca Lean benzeri sistemlerin RAM kullanımını küçümsemek de, Isabelle tarafındaki bellek oburluğu düşünülünce oldukça komik

    • Buradaki sorun, UNSAT sertifikasını hızla denetlenebilir bir biçime dönüştürmenin hiç de önemsiz olmaması
      Aslında bu neredeyse başlı başına biçimsel kanıt yazmak kadar zor
    • En son baktığımda Isabelle/HOL arayüz olarak özel bir Emacs modu kullanıyordu diye hatırlıyorum
      Başka bir HOL ile karıştırıyor da olabilirim
    • Sledgehammer’ın ne olduğunu bilmiyorum ama anlatılandan, Mathlib’deki grind ile neredeyse aynı türden bir araç gibi geliyor
      https://leanprover-community.github.io/mathlib4_docs/Init/Gr...

  • Lean’de ilginç olan şey, Lean’in bir dil olması ama insanların asıl konuştuğu şeyin çoğu zaman aslında Mathlib adlı kütüphane olması
    Mathlib’i yapanlar oldukça pragmatik görünüyor; bu yüzden de Lean tiplerinin içine klasik mantığı yerleştirip sezgici mantığı sadece kısmen kullanıyorlar gibi

    • Üçüncü halin imkânsızlığı anlatılırken verilen örnek yanlıştı
      “Bir şey aynı anda hem doğru hem yanlış olamaz” ifadesi üçüncü halin imkânsızlığı değil, çelişmezlik ilkesidir
      Üçüncü halin imkânsızlığı, p doğru ya da not p doğrudur demektir
      https://en.wikipedia.org/wiki/Law_of_noncontradiction
    • Bilgisayar bilimi tarafı artık kendi CSLib’ini oluşturuyor
      https://www.cslib.io https://www.github.com/leanprover/cslib
      Sezgici mantık özünde matematiksel akıl yürütmeyi hesaplanabilir yapılara dönüştürmekle ilgili olduğundan, bu meseleye nasıl yaklaşacakları ilginç
      Aslında Lean ile algoritma yazdığınız anda zaten bir şekilde yapıcı kısıtların içine giriyorsunuz ve o amaç için bu kadar mantık yeterli olabilir
    • Yapıcı matematiği kabullenmenin 5 aşaması esprisi aklıma geldi
      inkâr, öfke, pazarlık, depresyon, kabullenme
      Andrej Bauer’in ilgili konuşması ve yazısı da bakmaya değer
      https://www.youtube.com/watch?v=21qPOReu4FI
      http://dx.doi.org/10.1090/bull/1556
    • Burada kastedilen intuitive logic değil, intuitionistic logic olmalıydı
    • Bunca kısıt ve tıkanmaya rağmen, insanların ne zaman ve neden sezgici mantığı tercih etmeye başladığını merak ediyorum

  • Bence bu tür yazılara daha fazla ihtiyaç var
    Herkesin kendiliğinden doğruymuş gibi sadece X kullan diye dayattığı grup düşüncesine karşı, en azından alternatifleri değerlendirmek için her zaman ikna edici sebepler bulunabilir
    Sonunda alternatifi bırakıp ana akımı seçseniz bile, araziyi bilerek karar vermek daha iyidir

    • Buna tamamen katılmıyorum
      Şu anda bile çok fazla framework ve alternatif üretiyoruz; muhtemelen eğlenceli olduğu için daha da fazla üretiliyor
      Mevcut araçları iyileştirmek ya da sadece gerçek işi ilerletmek yerine, sürekli yeni dil, kütüphane ve derleme aracı eklemeye gidiliyor
      Bugünkü dil, kütüphane ve build tool sayısı yarısı kadar olsaydı bence daha iyi olurdu
    • Sonuçta duruma bağlı
      Ana akımdan ne kadar uzaklaşırsanız belge o kadar azalır, daha az keşfedilmiş köşeler yüzünden hata sayısı artar ve yardım alabileceğiniz insan sayısı düşer
      Seçenek sayısı yirmiyi geçtiğinde, ortalamada standart seçeneği alıp devam etmek doğrudur. Dikkat sınırlı; her bağımlılık için araştırma raporu yazarsanız asıl problemi çözemezsiniz
      İki istisna var: standart araç gerçekten benim kullanım durumuma uymuyorsa ya da standart aracın kendisi çözmeye çalıştığım temel sorunla büyük ölçüde çakışıyorsa

  • Bu tartışmalar bana Python’un bilimsel hesaplamadaki sınırlarını anlatan yazıları hatırlatıyor
    Yeterince iyi bir aracın etrafında topluluk kritik kütleyi aşacak kadar birikince, bu diğer unsurların çoğunu gölgede bırakıyor
    İvme oluşuyor; eğitimler, açıklayıcı yazılar ve daha iyi belgeler birikiyor ve sonunda fiilen kaçış hızına ulaşılıyor
    Lean, Terrance Tao gibi güçlü destekçileri de olduğu için tam şu anda böyle bir yerde gibi görünüyor
    O yüzden “X dili daha iyi” demek tamamen yanlış olmasa da asıl önemli soruyu kaçırmak kolay
    Esas mesele, herkesin bildiği, hemen kullanabildiği ve geliştirilmesine daha fazla zaman ayrılan araçtan gerçekte daha iyi olup olmadığı
    Sonuçta bu biraz worse is better ya da iyi ve popülerse bunun yeterli olduğu bir durum gibi görünüyor

    • LLM’lerin farklı biçimsel sistemler arasında çeviri işini oldukça etkili kılabilecek olması bence iyi bir nokta
      Özellikle bu alanda çeviri çıktısını büyük ölçüde otomatik doğrulamak mümkün olduğu için, seçim o kadar da büyük mesele olmayabilir
    • Ama AI çağında kritik kütlenin önemi çok daha az
      AI, devasa topluluk kütüphaneleri olmasa da kendi başına kod yazabilir ve internette milyonlarca eğitim metni dolaşmasa da belgeyi ve spesifikasyonu doğrudan okuyabilir
      İş piyasası olmayan dillerden kaçınmak da gerekmez. AI kariyer inşa etmiyor; sadece o anda verilen işi yapıyor
      Bu yüzden eskiden şansı olmayacak küçük diller ve DSL’ler için bile benimsenme ihtimali artıyor
      Programlamada uzun süredir devam eden dil tek kültürünü de AI’nin sona erdirebileceğini düşünüyorum

  • “Bugün herhangi bir sistemle biçimselleştirilen neredeyse her şey AUTOMATH ile de biçimselleştirilebilirdi” sözü, bugün modern dillerle yazılan her şeyin 50 yıl önce assembly ile de yazılabileceğini söylemeye benziyor
    Teknik olarak doğru olabilir ama ekonomik olarak tamamen farklıdır

    • Assembly dilleri genelde Turing-tamdır; kanıt motorları tarafında buna tam olarak karşılık gelen kıyasın ne olduğunu ben de pek bilmiyorum

  • Yaklaşık 15 yıl önce Coq/Rocq ve birkaç başka aracı kurcalamaya çalıştım ama kavramlardan çok yazılımın kendisini anlamak imkânsız gibi gelmişti
    Kanıt asistanları / etkileşimli teorem ispatlayıcılardaki tuhaflık şu: interactive olmaları yüzünden dil ve IDE birleşik bir hale geliyor ve pratikte de ikisi güçlü biçimde birbirine bağlanıyor
    Bu yüzden dili tek başına konuşmak zor; hangi ortamda kullanıldığına da bakmak gerekiyor
    Ben de VS Code’un fanatik bir hayranı değilim ama çok sayıda insanın kullandığı, büyük paralar harcanarak olgunlaştırılmış genişletilebilir IDE’nin alternatiflerin sunduğu ortamlardan çok ileride olduğu açık
    Natural Numbers Game gibi harika bir başlangıç yolu da sanki VS Code’un hacklenebilirliği ve ekosistemi sayesinde mümkün olmuş gibi
    Ama Lean öğrenirken beni kaygılandıran şey, söz dizimi genişletilebilirliğinin iki ucu keskin bir bıçak olması
    Dili öğrendikten sonra o dilde yazılmış kodu okumak istersiniz; ama projeler kendi DSL’lerini yığmaya başlarsa bu kontrolden çıkabilir
    Sonuçta bu, topluluğun ve ekosistemin ne kadar ölçülü davranacağına bağlı; o yüzden biraz umutla biraz da kaygıyla izliyorum

  • Lean, matematikçiler tarafından en çok sevilen kanıt asistanı da değil, yazılımın biçimsel doğrulanması için en uygun araç da değil
    Ama ikisini de idare eder düzeyde yapıyor ve karşılığında elde edilmesi en zor şey olan ivmeyi yakalamış durumda
    Üstelik AI çağında herkese açık insan eliyle yazılmış kod miktarı, ajanların yeni kodu ne kadar iyi üretebildiğini doğrudan etkilediği için, bu ivme daha da güçleniyor