Analysis I için Lean Companion

 (terrytao.wordpress.com)
2 puan yazan GN⁺ 2025-06-01 | 1 yorum | WhatsApp'ta paylaş
  • Terence Tao, gerçek analiz ders kitabı Analysis I’deki tanım, teorem ve alıştırmaları Lean koduna aktaran bir companion deposu başlattı
  • Doğal sayılar, tam sayılar, rasyonel sayılar, reel sayılar ile küme kuramı ve mantığı sıkı biçimde ele alan ders kitabı yapısı gereği, ispat yardımcısı ile öğrenmeye elverişli bir yapı sunuyor
  • Şu anki kapsam 2. bölümün bir kısmı, 3.1 temel küme kuramı ve 4.1 tam sayılara kadar uzanıyor; Mathlib doğal sayılarıyla izomorfizm de buna dahil
  • Kod Lean’de derleniyor, ancak birçok sorry hâlâ duruyor; resmî çözümler yerine bunların fork’larda doldurulması öneriliyor
  • Bu materyal, alıştırmaları Lean ile çözmek için alternatif bir yol olmasının yanında, ilerleyen bölümlerde Mathlib kullanımını öğrenmek için bir giriş kaynağı olarak da kullanılabilir

Analysis I’yi Lean’e taşıma projesi

  • Lean companion to “Analysis I”, Analysis I’deki çeşitli tanım, teorem ve alıştırmaları Lean’e “çeviren” bir proje
  • Kitaptaki alıştırmalar, Lean kodundaki karşılık gelen sorry kısımlarını doldurarak da çözülebilir
  • Resmî alıştırma çözümlerinin companion içinde barındırılması planlanmıyor; sorry doldurulmuş sürümler depo fork’ları olarak oluşturulabilir

Ders kitabı ile Lean neden iyi eşleşiyor?

  • Analysis I, mevcut gerçek analiz kitaplarını tamamlamak için temel meselelere daha fazla odaklanan bir ders kitabı
    • doğal sayıların, tam sayıların, rasyonel sayıların ve reel sayıların inşası
    • yüksek düzeyde titiz ispatlar geliştirmeyi mümkün kılan küme kuramı ve mantık
  • Kitap yazıldığı sırada Coq ve Agda gibi ispat yardımcıları zaten vardı, ancak o dönemde biçimsel doğrulama bir ilgi odağı değildi
  • Daha sonra biçimsel doğrulama deneyimi edinilince, kitabın içeriğinin ispat yardımcılarıyla iyi uyuştuğu görüldü
  • Kitapta standart sayı sistemleri inşa edilirken örtük olarak kullanılan naif tip teorisi, Lean’in bağımlı tip teorisiyle iyi örtüşüyor
  • Lean’in quotient type desteği de kitaptaki inşa biçimiyle uyumlu

Şu ana kadar Lean’e aktarılmış kapsam

Mathlib ile ilişkisi

  • Biçimselleştirme, bazı noktalarda standart Lean matematik kütüphanesi Mathlib’den ayrılıyor, diğer noktalarda ise Mathlib’e dayanacak şekilde tasarlanmış
  • Mathlib içinde zaten standart bir doğal sayı kavramı bulunuyor
  • Lean biçimselleştirmesinde önce doğal sayıları “elle” yeniden kuran Chapter2.Nat geliştiriliyor
    • Chapter2 namespace’i içinde çalışırken bu yapı Nat olarak kullanılabiliyor
    • Mathlib’deki doğal sayılarla ilgili yardımcı teoremlere paralel temel sonuçlar kuruluyor
    • Bunların birçok ispatı okur alıştırması olarak bırakılmış ve şu anda sorry ile değiştirilmiş durumda
  • Epilog bölümünde bu alternatif doğal sayılar ile Mathlib doğal sayıları arasındaki izomorfizm kuruluyor
    • daha doğrusu, bu izomorfizm de bir alıştırma olarak veriliyor
  • Bundan sonra 2. bölümdeki doğal sayı inşası artık kullanılmıyor ve Mathlib doğal sayıları kullanılıyor
  • Plan, kitabın ilerleyen bölümlerine geçildikçe önceki bölümlerdeki özel inşalardan ziyade Mathlib tanımları ve fonksiyonlarına daha fazla dayanma eğilimini sürdürmek

Kullanım biçimi ve doğrulama durumu

  • Depodaki kod Lean’de derleniyor
  • Ancak kod içindeki çok sayıdaki sorry ifadesinin gerçekten doldurulup doldurulamayacağı henüz test edilmiş değil
  • Gerekli yardımcı teoremlerin ya da Lean dosyalarının API’sinin yeterli olup olmadığının da doğrulanması gerekiyor
    • amaç, karmaşık Lean programlama tekniklerine bağımlı kalmadan sorry kısımlarının kavramsal olarak doğal bir şekilde doldurulup doldurulamayacağını görmek
  • Gönüllülerin companion’ı playtest ederek alıştırmaların gerçekten Lean içinde çözülebilip çözülemediğini kontrol etmesi isteniyor
  • Diğer geri bildirimler de memnuniyetle karşılanıyor

Lean·Mathlib’e giriş kaynağı olarak niteliği

  • Bu companion, yalnızca gerçek analiz için değil, Lean ve Mathlib’e giriş için de kullanılabilir
  • Bu yönüyle Natural number game ile bir ölçüde benzerlik taşıyor
  • Natural number game, konu olarak Analysis I’in 2. bölümüyle önemli ölçüde örtüşüyor

İlgili okumalar

1 yorum

 
GN⁺ 2025-06-01
Hacker News yorumları

  • Matematiği Lean ile öğretirken en ilginç noktanın anında geri bildirim olduğunu düşünüyorum. Öğrencinin ispatı yanlışsa, basitçe derlenmiyor.
    Eskiden geri bildirim alabilmek için bir asistanın, eğitmenin ya da uzmanın bakması gerekirdi; artık Lean derleyicisi hızlıca geri bildirim verebiliyor.
    İleride Rust derleyicisinin kod düzeltme önerileri sunması gibi Lean derleyicisinin de daha eğitici geri bildirimler sağlaması güzel olurdu; belki bunun için özel bir LLM gerekebilir.

    • Neredeyse tamamen katılıyorum, ama ispat öğrenirken yavaş düşünmenin eksik kalabileceği konusu kafama takılıyor.
      Eskiden matematik çalışırken ödevin başında kâğıt üzerinde çeşitli şeyler deneyip uzun uzun düşünmeye çok zaman ayrılırdı; bu süreç bazen kavramların içselleştirilmesine ve yeni fikirlere yol açardı.
      Lean kullanınca, rastgele denemeler yapıp kontrol ederek bir şeyler dökme tarzına dönüşebilir mi diye düşünüyorum. Coq ile birkaç kez uğraştığımda da çoğunlukla orasını burasını kurcalayıp denediğimi hatırlıyorum.
    • Acorn zaten bu şekilde çalışıyor. Bir ispat başarısız olduğunda ama “neredeyse doğru”ysa, VS Code içinde şuna benzer öneriler gösteriyor:
      reduce(r.num, r.denom) = reduce(a, b)
      cross_equals(a, b, r.num, r.denom)
      r.denom * a = r.num * b
      LLM kullanmıyor; VS Code eklentisinin içinde küçük bir yerel model çalışıyor. Umarım bir gün o küçük yerel model insanları açık ara aşacak kadar güçlü hâle gelir. Ayrıntılar https://acornprover.org/docs/tutorial/proving-a-theorem/ adresinde.

  • Gerçekten heyecan verici. Ayrı bir depoya taşınır da bulması ve başkalarına göndermesi kolaylaşırsa güzel olur.
    Zaten matematiği merak ediyordum; Tao’nun Analysis kitabı, programlama zihnimin beklediği titiz biçimde matematiğin nasıl kurulduğunu bana ilk gösteren ders kitabıydı.
    Sonrasında Lean’i de biraz denedim ve benzer şekilde tatmin ediciydi; ama Mathlib, matematik kavramlarını öğrenmek için epey karmaşıktı. Bu yüzden kitap ile araç arasında bir köprü kurulmasına seviniyorum.

    • Ben de yakınsama, Cauchy dizileri gibi konuları o kitaptan öğrendim. Hindustan Book Agency adlı yerel, kâr amacı gütmeyen bir yayınevinden çıkmıştı ve fiyatı da çok uygundu.

  • Analiz gibi ana akım matematik konularında teorem ispatlamanın ivme kazandığını görmek güzel.
    Programlama dili kuramı tarafında, araçların 2010’ların ortalarında epey olgunlaşmaya başladığı dönemde, Winskel’in The Formal Semantics of Programming Languages gibi temel bir ders kitabı Isabelle ile biçimsel olarak doğrulanmıştı. Tam bir 1:1 aktarım değil ama http://concrete-semantics.org bunun bir örneği.
    Teorem ispatlamaya ilgi duyuyorsanız, şahsen oranın çok daha kolay bir başlangıç noktası olduğunu düşünüyorum. Çünkü analiz teoremleri kendi başlarına zaten oldukça zor.

    • Programlama dili ispatlarının giriş için daha kolay olması şaşırtıcı değil. İnsanların dediği gibi, çok daha fazla biçimselleştirilmiş prosedür var gibi görünüyor.
      Yapısal indüksiyon yapıp, indüksiyon varsayımını uygulayarak değişmezin korunduğunu gösteriyor ve böyle devam ediyorsunuz.
      Çok fazla teorem ispatı yapmış da değilim, ispat yardımcılarıyla analiz gibi “matematiksel” ispatlar da yapmadım; ama matematik ispatları çok daha farklı bir yaklaşım gerektiriyorsa, ikisi arasında beceri aktarımının ne kadar olduğunu merak ediyorum.
      Rocq’nun Software Foundations’ını da anmak isterim. Lean portu olabilir, ama baş kısımlarını takip ettiğimde oldukça rahat ilerlemişti.

  • Ana akım “ders kitabı” yaklaşımının Mathlib yaklaşımından nasıl farklı olduğunu değerlendirmek çok ilginç olurdu.
    Genel olarak biçimselleştirilmiş matematik kütüphaneleri sonuçları mümkün olduğunca genel ifade eder ve ispat akışını daha sezgisel, daha zarif biçimde yeniden düzenlemeyi kolaylaştırır.
    Yeniden düzenlemenin kolay olmasının nedeni, sistemin neyin neyden mantıksal olarak çıktığını her zaman izlemesidir. Kâğıt kalemle çalışırken bu olmadığı için yeniden çalışma fırsatları sıkça kaçırılır.
    Lisans düzeyinde Mathlib tarzı “azami genellik” sürümündeki reel analizi öğretmenin mantıklı olup olmadığı da doğal bir soru. Elbette ispat temelli matematiğin diğer alanları için de aynı şey geçerli.

    • Giriş dersi için kesinlikle hayır derim. Zaten öğrenilecek çok şey var: ispat yapmayı öğrenmek, programlama yapmayı öğrenmek ve asıl ders içeriği.
      Bildiğim kadarıyla bunu gerçekten deneyen öğretim üyelerinin deneyimi de benzer. İleri düzey öğrenciler için uygun olabilir, ama ortalama bir öğrenci için ders zamanını boşa harcama ihtimali yüksek.
    • Hem matematikçi hem de uzun süredir programlama yapan biri olarak, herhangi bir program tarzı biçimcilik temel anlayışı yerleştirmekte başarısız olacak gibi geliyor.
      Benim önyargım, matematik kavramlarını makalelerden öğrenmiş olmamdan geliyor.
      Kodun muazzam bir ek yük getirdiğini ve çoğu zaman herhangi bir stil standardına uymadığını hissediyorum. Anlaşılmaz diye değerlendirilen matematik makalelerini de okumak zorunda kalmış biri olarak söyleyeyim: Kodda anlaşılabilirlik standardı fiilen neredeyse hiç olmadığı için 10 kat daha kötü.

  • Terence Tao’nun kendi YouTube kanalında da Lean kullandığı birkaç video var. https://www.youtube.com/@TerenceTao27
    Ayrıntıları bilmiyorum ama LLM kullanarak ya da kullanmadan çalışmasını izlemek güzeldi.

  • Analiz gibi temel bir konu için çok iyi bir proje ve iyi bir yaklaşım olduğunu düşünüyorum.
    Aklıma hemen gelen iki endişe var. Birincisi, Mathlib’in temel analiz sonuçları limitleri genel ve birleşik biçimde ele almak için filtre kavramını kullanıyor. Yine de bazı sonuçlar epsilon-delta biçimine özelleştirilmiş durumda. Tao’nun Analysis kitabının daha geleneksel epsilon-delta yaklaşımını kullanacağını düşünüyorum.
    İkincisi, Mathlib hızlı ilerliyor ve sık sık kırılıyor. İsimler değişiyor, yeniden düzenlemeler sürekli oluyor; bu yüzden alt depoların sürekli bakıma ihtiyacı var.

  • Oldukça radikal bir fikir ama matematik eğitiminin, Mathematica gibi bilgisayar cebiri sistemleri ve Lean gibi teorem kanıtlayıcılar geliştirmeye odaklanması gerektiğini düşünüyorum. Görselleştirme ve pratik uygulamalar da güçlü biçimde dahil edilmeli
    Uç noktada, kâğıt üzerinde hiç matematik yapmadan, öğrenilen her şeyi Lean içinde kanıtlayabilir hâle gelmek gibi bir biçim alabilir
    Mevcut sistem bitmek bilmeyen elle hesaplamalara odaklanıyor; bunun çok işe yaramaz göründüğünü ve sıkıcı olduğu için insanları matematikten soğuttuğunu hissediyorum

  • Lean ders kitabı olması güzel. Peki neden HoTT yok?
    “Should Type Theory (HoTT) Replace (ZFC) Set Theory as the Foundation of Math?”
    https://news.ycombinator.com/item?id=43196452
    Bu hafta HN’de çıkan ek Lean kaynakları:
    “100 theorems in Lean”
    https://news.ycombinator.com/item?id=44075061
    “Google-DeepMind/formal-conjectures: collection of formalized conjectures in lean” https://news.ycombinator.com/item?id=44119725

    • HoTT’deki çeşitli fikirlerin biçimselleştirilmesi şu anda Agda topluluğunda yürütülüyor. https://martinescardo.github.io/HoTT-UF-in-Agda-Lecture-Notes/
      Kesin motivasyon benim alanımın dışında olduğu için bilmiyorum ama Agda, bu fikirleri biçimselleştirmek için Lean’den daha uygun bir yol gibi görünüyor
      Bu yılın sonlarında, mevcut HoTT kitabının daha modern bir güncellemesi sayılabilecek yeni bir ders kitabı da çıkacak; bunun Agda biçimselleştirmesi de var
      https://www.cambridge.org/core/books/introduction-to-homotopy-type-theory/0DD31EC06C80797A50ACE807251E80B6
      https://github.com/HoTT-Intro/Agda
    • HoTT çok teknik ve çok dar bir konu; bu şekilde iki iddialı projeyi aynı anda ele almak mantıklı değil
      HoTT, makul bir standart olarak kabul edilmeye hiç yakın değil ve çoğu insan için daha en baştan tıkanma noktası olan bir konu
      Bu, bir JavaScript framework geliştiricisine neden Elm ya da Haskell için framework yapmadığını sormaya benziyor
    • HoTT’nin neden olması gerektiğini de bilmiyorum
      HoTT teorem kanıtlayıcılarını kullanımı rahat hâle getirmek için harcanan emek çok daha az, belgeleri de çok daha zayıf
      HoTT’nin faydaları da belirsiz. Kategori teorisinin çok anlaşılması güç yapılarıyla uğraşırken ancak işi azaltıyor gibi görünüyor
    • “Neden HoTT yok?” sorusu biraz garip
      Terrence Tao’nun analiz üzerine birkaç ders kitabı var ve bu da ilk kitabı için hazırlanmış Lean eşlik materyali. Onun tip teorisi üzerine bir ders kitabı yok; dolayısıyla yüksek dereceli tip teorisi de yok. Zaten yapılmak istenen şey tamamen farklı
    • Mevcut bir ders kitabına eşlik eden materyal olması bile “neden HoTT değil?” sorusunu yanıtlıyor. Bir başka neden de insanların bunun eğitimsel değerinden şüphe duyması olabilir

  • Çok hoş. Analysis I, matematikçi değil mühendis olan benim, Rudin gibi başka kitapları birkaç kez denedikten sonra ilk kez tamamen takip edip çözebileceğimi hissettiğim “gerçek” matematik ders kitabıydı
    Umarım Lean eşlik materyali, matematiğe ve programlamaya aşina olup konuyu titizlikle öğrenmek isteyenler için bunu daha erişilebilir kılar

  • Son birkaç yıldır Tao’nun Analysis I kitabını Lean’da biçimselleştirmeye yönelik düzenli girişimler oldu; hatta şu anda Tao’nun yaptığı şeyin aynısını yapmaya çalışan insanlar vardı. Ne yazık ki çoğu ilk birkaç bölümün ötesine geçemedi; umarım Tao daha ileri gidebilir
    Ben de bunu kendim denemeyi düşünmüştüm. Analysis I açıklama blogumda https://taoanalysis.wordpress.com/ her alıştırmanın biçimselleştirilmiş kanıtını eklemek, kitabı takip edenler için faydalı olur diye düşündüm
    Kitabın özel Discord sunucusunda da paylaştım ama burada da işe yarayabileceğini düşünerek ilgili kaynakları paylaşıyorum
    https://github.com/cruhland/lean4-analysis — https://github.com/cruhland/lean4-axiomatic adresinden alınmış
    https://github.com/Shaunticlair/tao-analysis-lean-practice
    https://github.com/vltanh/lean4-analysis-tao
    https://github.com/gabriel128/analysis_in_lean
    https://github.com/mk12/analysis-i
    https://github.com/melembroucarlitos/Tao_Analysis-LEAN
    https://github.com/leanprover-community/NNG4/ — Tao’nun kitabını takip etmiyor ama Lean4 sürümü bir doğal sayılar oyunu olduğu için içeriği 2. bölüme çok benziyor
    https://github.com/djvelleman/STG4/ — Lean4 küme teorisi oyunu olduğundan 3. bölüme benzeyebilir. Ancak https://github.com/djvelleman/STG4/blob/main/Game/Metadata.lean içinde import Mathlib.Data.Set.Basic göründüğü için, kümeleri baştan tanımlayıp aksiyomlar kurmak yerine Lean’in kümelerini içe aktarıyor gibi duruyor. Bu yaklaşım, Lean’in küme teorisi hakkında “fazla fazla” şey bilmesine yol açabileceğinden amaç için uygun olmayabilir
    https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc — tam sayıları oluşturmak için
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/IntegerGame.lean — yukarıdakiyle aynı dosya olabilir
    https://github.com/ImperialCollegeLondon/IUM/blob/main/IUM/2023/RationalGameAlgebra.lean — rasyonel sayıları oluşturmak için
    https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality — kullanıcı tanımlı bir Set tipi tanımlamanın bir yolunu gösteriyor