Lean: Modern Formal Matematik Dili

"Matematik yazılım gibi"

Klasik matematik kağıt-kalem. Bir ispat:

"Eğer $n$ tek sayıysa, $n^2$ tektir. Çünkü $n = 2k+1$ ise $n^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$, ve bu tek sayıdır."

Bu insan dili. Bilgisayar doğrulayamaz. Eğer yanlış varsa, hakem (insan) tespit etmeli.

Modern formal matematik bunu değiştiriyor: ispatlar yazılım gibi yazılır. Lean bunun en popüler dili.

Lean nedir

Lean theorem prover — Microsoft Research'ten Leonardo de Moura tarafından 2013'te tanıtıldı.

Lean ispatları Lisp/Python'a benzer sözdizimi ile yazılır:

theorem odd_square (n : Nat) (h : Odd n) : Odd (n * n) := by
  rcases h with ⟨k, hk⟩
  use 2 * k^2 + 2 * k
  rw [hk]
  ring

Bu kod mantıksal olarak doğrulanmış ispat. Lean derleyici "TAMAM" derse ispat kesinlikle doğru.

Niye önemli

Klasik matematik ispatları zaman zaman yanlış:

• Eski makalelerde hatalar bulunur.
• Karmaşık ispatlar denetlenemez.
• "Bu kısımları okuyucuya bırakırız" deyişi.

Formal matematik bu sorunları çözer:

• İspat doğrulanmamışsa derleyici reddeder.
• Her adım açık.
• Yanlış olamaz.

Mathlib — matematiğin GitHub'i

Mathlib — Lean için açık matematik kütüphanesi. Kullanıcı topluluğu binlerce teoremi formal olarak ispatlamış.

İçerik:

• Lineer cebir.
• Analiz.
• Topoloji.
• Sayı teorisi.
• Cebirsel geometri.
• Kategori teorisi.

Mathlib matematik tarihinin formal sözlüğü olarak büyüyor. 2024 itibariyle 100K+ teorem.

AI için temel

Lean ve Mathlib, AI matematiğinin eğitim verisi:

• AlphaProof: Lean üzerinde eğitildi.
• GPT-f: OpenAI'nin önceki matematik AI'sı.
• Llemma: Açık kaynak matematik LLM.

Sebep: Lean doğru/yanlış ispatları net ayırır. AI denemeleri öğrenebilir.

Modern matematik etkileri

Lean modern matematik üzerine etki yapıyor:

1. Liquid Tensor Experiment (2020)

Peter Scholze (Fields Madalyalı) bir ispatın doğruluğundan emin olmak için Lean topluluğa isim verdi: "bu ispatı Lean'da doğrulayın." Yaklaşık 1 yıl sonra başardılar.

Bu, modern matematiğin denetleme aracı.

2. Mathematics Wiki

Lean ispatları paylaşılabilir. Tarihsel ispatlar formal hâle getiriliyor.

3. AI matematik

AlphaProof + Lean kombinasyonu AI + insan matematikçi işbirliğinin temeli.

Diğer formal diller

Lean tek değil. Alternatifler:

• Coq: Fransa'da. Eski (1989).
• Isabelle/HOL: Daha matematiksel.
• Agda: Tipik akademik.

Lean popülerleşmesi: modern dil tasarımı + Mathlib topluluğu + Microsoft desteği.

"Matematiğin yeniden yazılması"

Bazı görüşler: bütün matematik Lean'da formal yazılmalı. Bu 100+ yıllık proje.

Avantajı: matematik yanlışlardan tamamen temizlenmiş.

Dezavantaj: muazzam iş, insan matematikçi kalır mı?

Modern AI ile bu vizyon değişti. AI Lean'da ispatları otomatik üretebilir. 100 yıllık vizyon belki 20.

Sade ders

Lean hikâyesinden iki şey:

1. Formal matematik klasiği değiştirebilir. Klasik matematik insan dili; Lean bilgisayar mantığı. İkisi farklı bilim disiplinleri gibi.
2. AI + formal matematik = yeni paradigma. AlphaProof Lean ile çalışır. Bu birleşim modern matematiğin nasıl yapıldığını kalıcı olarak değiştirecek.

Bağlam

AlphaProof için: [[alphaproof-ai-matematik-olimpiyatinda-gumus-madalyaya]]. Tim Gowers için: [[tim-gowers-fields-madalyali-matematikcinin-ai-ile-bulusmasi]]. Terence Tao için: [[terence-tao-yasayan-en-buyuk-matematikci]]. AI4Science için: [[ai-icin-bilim-protein-ilac-malzeme-yeni-aydinlanma]]. Chain-of-thought için: [[chain-of-thought-llm-leri-akil-yurutmeye-zorlamak]].