Analysis I için Lean yardımcı kaynağı

• Terence Tao’nun yazdığı gerçek analiz ders kitabı Analysis I’in temel içeriğini Lean ispat yardımcısına aktaran bir projedir
• Bu proje, temel sayı sistemlerinin inşası ve ispat mantığı gibi, özgün eserin titizliği vurgulayan hedefleriyle iyi örtüşen bir yapıya sahiptir
• Mathlib standart kütüphanesinden yararlanırken, ana kavramların doğrudan inşa edilmesi ve okurun bizzat ispat yaparak pratik yapması da dahildir
• Lean kodundaki boşlukları (sorry) doğrudan doldurarak pratik yapılabilir; resmî çözüm verilmez ve fork edilerek genişletilebilir
• Hem Lean’a yeni başlayanlar hem de gerçek analiz öğrenenler için Mathlib ve Lean’in pratik kullanımını deneyimleme fırsatı sunar

---

Genel bakış

• Terence Tao’nun yazdığı gerçek analiz kitabı "Analysis I"i Lean ispat yardımcısı aracı ile yeniden kurgulayan bir açık kaynak projedir
• Bu ders kitabı, diğer analiz kitaplarının çoğuna kıyasla doğal sayılar, tam sayılar, rasyonel sayılar ve gerçek sayıların inşa sürecine, ayrıca bu süreçte gereken küme kuramı ve mantıksal araçlara daha fazla odaklanır
• Kitabın büyük kısmı sistematik biçimde titiz ispat yapabilme becerisi geliştirmeye odaklandığından, Lean gibi bir ispat yardımcısıyla çok uyumlu bir yapı sunar

Lean yardımcı proje özellikleri

• Özgün eserdeki tanımları, teoremleri ve alıştırmaları Lean biçimine "çevirerek" sunar
• Bu Lean dosyalarında, alıştırma çözümlerine karşılık gelen çok sayıda boşluk (sorry) bulunur; bunlar okur tarafından doldurularak öğrenme sağlanır
• Resmî açıklamalar (çözümler) sunulmaz; ancak okur depoyu fork ederek kendi çözüm sürümünü oluşturabilir

Mathlib ile bağlantı ve farklılıklar

• Mathlib’de (Lean’in standart matematik kütüphanesi) zaten uygulanmış kavramlar (ör. doğal sayılar) özellikle yeniden doğrudan kurulur; ardından Mathlib sürümüyle izomorfizminin (eşdeğerliğinin) ispatlanması da sürecin parçası olur
• Örneğin Chapter2.Nat içinde, Mathlib’in doğal sayılarından ayrı kendi doğal sayı tanımı en baştan kurulur; temel sonuçlar doğrudan ele alındıktan sonra, sonda iki sürümün eşdeğer olduğunu Lean içinde pratik ederek gösterme imkânı verilir
• Sonraki bölümlerden itibaren Mathlib’in tanımları ve işlevleri giderek daha fazla kullanılmaya başlanır

Öğrenme ve kullanım yöntemi

• Bu Lean yardımcı kaynağı, yalnızca analiz öğrenimi için değil, Lean ve Mathlib içinde matematiğin nasıl formelleştirildiğine dair bir giriş işlevi de görür
• "Natural number game"de olduğu gibi, Lean ortamında matematiksel nesneleri doğrudan tanımlayıp pratik yapmaya imkân veren yapılandırılmış alıştırmalar içerir
• Kodun kendisi Lean’de derlenebilir; ancak tüm alıştırmaların (sorry) gerçekten çözülebilir olup olmadığı tam doğrulanmış değildir, bu nedenle playtest ve geri bildirim gereklidir

Açık kaynak ve katkı

• Depo açık kaynaklıdır; herkes inceleyebilir, fork edebilir ve katkı sunabilir
• Resmî çözümler ayrıca verilmez; birden fazla çözüm sürümünün oluşturulmasını destekler
• 31 Mayıs itibarıyla proje ayrı, bağımsız bir depoya taşınmıştır

[GN⁺]

Hacker News yorumları

• Bu durum beni gerçekten heyecanlandırıyor; özellikle bu proje bağımsız bir repo'ya taşınırsa başkalarıyla paylaşmanın ve keşfetmenin çok daha kolay olacağını düşünüyorum. Matematiğe hep merakım vardı ve Tao'nun Analysis kitabı, matematiğin ne kadar katı bir biçimde inşa edildiğini programlama düşünce tarzıma uygun şekilde bana ilk kez gösteren ders kitabı olmuştu. Sonrasında Lean'e de merak sardım ama Mathlib ile matematiksel kavramları öğrenmenin biraz karmaşık olduğunu hissettim. Bu yüzden kitapla araç arasında köprü kuran bu projeyi gerçekten çok beğeniyorum.

  • Benim de benzer bir deneyimim oldu; yakınsaklık, Cauchy dizileri vb. öğrenmiştim ve bu kitabın Hindistan'daki kâr amacı gütmeyen yayınevi Hindustan Book Agency tarafından basılması sayesinde çok ucuza edinilebildiğini hatırlıyorum.

• Lean kullanılarak verilen matematik eğitiminde bana en heyecan verici gelen şey anında geri bildirim sağlaması. Öğrenci bir ispatı yanlış yazarsa derlenmiyor. Eskiden böyle geri bildirim için asistan ya da hocanın doğrudan bakması gerekirdi, şimdi ise Lean derleyicisi bunu hızlıca söyleyebiliyor. İleride Rust derleyicisinde olduğu gibi daha dostça düzeltme önerileri de sunmasını isterim (bunun için özel bir LLM gerekebilir).

  • Buna büyük ölçüde katılıyorum ama ispat üzerine düşünme sürecinin de önemli olduğunu düşünüyorum. Matematik deneyimim eskiye dayanıyor ama ödevleri ve problemleri kâğıda yazarak yavaş yavaş düşündüğüm, adeta bir "matematik cenneti" gibi geçen çok zamanım oldu. Lean kullanınca bunun yerine rastgele girdiler deneme ya da otomatik olarak tutana kadar uğraşma gibi daha "parmak egzersizi" ağırlıklı bir sürece kayılmasından endişe ediyorum. Eskiden coq'u kısa süre denemiştim ve neredeyse sürekli bir şeyleri kurcalayıp durduğumu hatırlıyorum. Kısacası theorem solver'ların birçok yönden faydalı olduğunu düşünüyorum ama bu yavaşça sindirme sürecinin kaybolmasıyla içselleştirme, kavramsallaştırma ve yeni fikir üretme yollarının zayıflayabileceğinden endişeliyim. Bu konuda başkalarının ne düşündüğünü merak ediyorum.

• Terence Tao'nun Lean'i doğrudan kullandığı videoların bulunduğu kişisel bir YouTube kanalı olduğu söylenmiş. Bu alanın uzmanı değilim ama LLM ile ya da LLM olmadan çalışmasını izlemek bile bana çok ilginç geldi (https://www.youtube.com/@TerenceTao27).

• Geleneksel "ders kitabı tarzı" yaklaşımı Mathlib yaklaşımıyla karşılaştırıp değerlendirmek gerçekten ilginç olurdu. Formel matematik kütüphaneleri genelde sonuçları olabildiğince genel biçimde ifade eder ve ispat yapısının kendisini refactor ederek daha zarif hale getirmek de kolaydır. Refactor yapmak kolaydır çünkü sistem mantıksal bağımlılıkları sürekli takip eder; bunu sadece kâğıt kalemle yapmak kolay değildir. Bu yüzden Mathlib'deki gibi "azami genellik" düzeyindeki analiz yaklaşımının üniversite derslerinde öğretilmesinin uygun olup olmadığı doğal bir soru gibi geliyor. Bunun, ispat temelli matematiğin diğer tüm alanları için de geçerli bir mesele olduğu söyleniyor.

  • En azından giriş seviyesindeki dersler için uygun olmadığını düşünüyorum. Müfredatta zaten eklenecek çok fazla şey var — ispat yöntemleri, programlama yöntemleri ve temel kuram. Gerçekten denemiş hocaların deneyimleri de benzer; ileri düzey öğrenciler için iyi olsa da ortalama öğrenci için zaman kaybı olarak görüldüğünü düşünüyorum.

  • Uzun zamandır programlama da yapan bir matematikçi olarak, herhangi bir programatik formelleştirmenin temel anlayışı kendi başına geliştireceğini sanmıyorum. Önyargım biraz da kavramları makaleler üzerinden öğrenmiş olmamdan geliyor. Kod, stil kaygısı taşımadığında okunabilirlik açısından çoğu zaman bunaltıcı olabiliyor; okunması zor makaleler zaten yeterince zor, ama kodda standart bile olmayınca bana göre bu 10 kat daha zor hale geliyor.

• Teorem ispatının analiz gibi ana akım matematik alanlarında giderek daha fazla ilgi görmesi sevindirici. PLT'de zaten Winskel'in The Formal Semantics of Programming Languages adlı önemli kitabının Isabelle ile formel olarak doğrulanmış bir örneği vardı (http://concrete-semantics.org). Eğer teorem ispatına başlamak istiyorsanız, o tarafın daha kolay ve daha tavsiye edilebilir olduğunu düşünüyorum. Analizdeki teoremlerin doğası gereği zaten oldukça zor olduğunu da eklemek gerekir.

  • PL ispatlarının giriş bariyerinin daha düşük olmasına ben de şaşırmam. Bunun daha rutin bir his verdiği de sık söylenir — yapısal tümevarım, tümevarım uygulama, invariant ispatı, tekrar vb. Ben çok fazla teorem ispatı yapmadım ve özellikle analiz gibi "matematiksel" ispatları bir theorem prover ile hiç denemedim. "Matematiksel" ispatlar gerçekten çok farklı bir yaklaşım mı gerektiriyor ve iki alan arasında beceri aktarımı ne kadar mümkün, bunu merak ediyorum. Bu arada Rocq içindeki Software Foundations'ı çalışmıştım (belki Lean'e taşınmış bir sürümü de vardır?) ve oldukça keyif almıştım.

• Bu proje ve yaklaşımın analiz gibi temel konulara çok iyi uyduğunu düşünüyorum. Ama iki endişem var

  1. Mathlib, analizin temel sonuçlarını filter kavramı üzerinden birleşik biçimde ele alıyor; özel durumlar ise ayrıca epsilon-delta tarzında işleniyor. Tao'nun Analysis kitabının daha geleneksel epsilon-delta yaklaşımını kullanacağını tahmin ediyorum.
  2. Mathlib çok hızlı değişen bir proje, dolayısıyla adlar ve yapı sürekli değişiyor. Eşleştirme bilgisinin sürekli bakım gerektirmesi kaçınılmaz.
  • Herkesin kendisinin de kontrol edebileceği belirtilmiş; gerçekten de dizilerin limitine dair bölümün büyük kısmı örnek sayfa olarak açık durumda, ilgilenenler şu bağlantıya bakabilir: https://link.springer.com/chapter/10.1007/978-981-19-7261-4_6

• Çok harika bir proje gibi görünüyor. Analysis I, mühendis olan benim gerçekten ilk kez baştan sona takip ederek çalışabildiğim "gerçek" matematik ders kitabıydı; başka kitaplara (Rudin vb.) defalarca başlayıp başaramamıştım. Bunun Lean sürümü olursa, hem matematiğe hem programlamaya aşina insanların kavramları daha katı biçimde öğrenmesine yardımcı olabilir diye umutluyum.

• Yıllardır Tao'nun Analysis I kitabını resmî olarak Lean ile formelleştirme girişimleri oldu ama hep birkaç bölümün ötesine geçmekte zorlanıldı. Bir dönem ben de bunu kendim denemek istemiştim — Analysis I çözümleri bloguna (https://taoanalysis.wordpress.com/) bağlantılı formel ispatlar da eklenirse, kitaptan çalışanlar için çok faydalı olur diye düşünüyordum. Zaten özel bir Discord'da bazı düzenlemeleri paylaşmıştım; burada da başkalarının işine yarayabilecek çeşitli referans Lean projelerini (github, gist, resmî dokümanlar vb.) topluca paylaşıyorum:

  • https://github.com/cruhland/lean4-analysis
  • https://github.com/cruhland/lean4-axiomatic
  • 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/ (bu Tao'nun kitabı değil, Natural Number Game'in Lean4 sürümü; içerik olarak 2. bölümle neredeyse aynı)
  • https://github.com/djvelleman/STG4/ (benzer şekilde bir set theory game; 3. bölümle benzer, ama Game/Metadata.lean dosyasında import Mathlib.Data.Set.Basic kullanıldığı görülüyor, yani küme kuramı tamamen baştan tanımlanmıyor, içe aktarılıyor — bu durumda Lean küme kuramını zaten "biliyor" olduğu için bizim amaçlarımız açısından tam uygun olmayabilir)
  • https://gist.github.com/kbuzzard/35bf66993e99cbcd8c9edc4914c9e7fc (tam sayıları kurma örneği)
  • 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ı kurma örneği)
  • https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#function-extensionality (özel bir Set türü tanımlamak için başvuru örneği)

• "Mathlib'deki karşılık gelen nesneyle izomorfizm ispatı"nın pratikte ne kadar önemli olacağını merak ediyorum. Acaba izomorfizm kısmı çıkarılsa fiilen hiçbir şey değişmez mi? Örneğin teoremleri otomatik çevirmek gibi şeylerde gerçekten işe yarıyor mu?

  • Bu tür izomorfizm ispatları

    1. Kendi oluşturduğunuz nesne ile Mathlib'de zaten bulunan nesnenin gerçekten aynı olduğunu ispatlamanızı sağlar; özellikle Mathlib tarafında bunlar oldukça genelleştirilmiş yapılarla tanımlanmış olabileceğinden, farkları anlamaya yardımcı olur.
    2. Mathlib'de o nesneleri okurken veya yazarken kullanılan resmî gösterim ve terminolojiyi anlamak açısından kritik rol oynar.

  • En azından eğitsel bir değeri olduğunu düşünüyorum. Kitap içinde sizin kurduğunuz küme ve işlemlerin başka yerlerde de "aynı şey" olduğuna bizzat ikna olma süreci anlamına geliyor.

• Lean tabanlı bir ders kitabının çıkması sevindirici, ama neden HoTT (Homotopy Type Theory) yok? "Type Theory (HoTT), (ZFC) küme kuramının yerini almalı mı?" başlıklı bir tartışma da vardı (https://news.ycombinator.com/item?id=43196452). Bu hafta HN'de çıkan ek Lean topluluk kaynakları da paylaşılmış — "100 theorems in Lean" (https://news.ycombinator.com/item?id=44075061) ve DeepMind Lean projesi (https://news.ycombinator.com/item?id=44119725).

  • Ama neden özellikle HoTT olması gereksin, onu pek anlamıyorum. HoTT theorem prover'larının kullanıcı deneyimi hâlâ zayıf, dokümantasyon da yeterli değil. Ayrıca HoTT'nin sağladığı fayda da bana çok net görünmüyor; genelde sadece kategori teorisi gibi aşırı özel yapılarla uğraşırken anlamlı olduğu yönünde bir görüş var.

  • Zaten mevcut ders kitabı yaklaşımı olduğu için "neden HoTT değil" sorusunun cevabı bunun içinde saklı. Ayrıca bunun eğitsel faydasına şüpheyle yaklaşan çok sayıda uzman olduğunu da düşünüyorum.