Leonardo de Moura: Lean'in Mucidi, Brezilyalı Akademisyen
Brezilya kökenli Microsoft Research araştırmacısı, modern formal matematiğin altyapısı Lean'i yaratan figür.
"Lean'in babası"
Leonardo de Moura Lean theorem prover'in yaratıcısı. AlphaProof, AI matematik, formal matematik ekosisteminin altyapısı.
de Moura Brezilya kökenli bir akademisyen. Modern AI tarihinde az sayıda Brezilyalı figürlerden biri.
São Paulo'dan Microsoft'a
de Moura 1964 Brezilya doğumlu. São Paulo Üniversitesi'nde mühendislik. PUC-Rio'da doktora.
Doktora konusu: otomatik teorem ispatlama. Klasik akademik konu, formal verification.
1998'de Microsoft Research'a katıldı. 25+ yıl orada.
Z3 — modern SAT solver
de Moura'nın ilk büyük başarısı: Z3 SMT solver (2007). Boolean satisfiability + theory reasoning.
Z3 modern formal verification'in standard araçı. Yazılım doğrulama, donanım tasarım, AI güvenliği. Akademik + endüstri kullanılır.
Lean (2013)
de Moura 2013'te Lean theorem prover'i başlattı. Hedef: kullanıcı dostu formal matematik dili.
Klasik formal matematik (Coq, Isabelle) zor. de Moura'nın felsefesi:
"Matematikçi için kolay olmalı. Bilgisayar bilimi için hızlı. İkisi birlikte."
Lean bu dengeyi sağladı. 10 yıl sonra Mathlib 100K+ teorem.
Lean 4 (2021)
Lean 4 majör yeniden tasarım. Programlama dili olarak kullanılabilir + theorem prover.
Bu yeniden tasarım Lean'i modern dil yaptı. Topluluk hızla büyüdü.
"Akademik açık"
de Moura akademik tarzı: açık, kollaboratif. Mathlib topluluğu binlerce kişi kapsayan açık akademik proje.
Bu, klasik akademik "izole laboratuvar" tarzından çok farklı.
AWS'e geçiş (2023)
2023'te Microsoft Research'ten Amazon AWS'e geçti. AWS'te formal verification cephesinin başı.
Bu geçiş tarihinde AlphaProof tam patlamıştı. de Moura AWS'e geldikten sonra Lean ve formal AI matematik üzerine çalışma sürdürdü.
Sade ders
de Moura hikâyesinden iki şey:
- Brezilya AI cephesi var ama az. Brezilyalı akademisyenler ABD'ye geçer. Yerel AI ekosistemi sınırlı. de Moura gibi figürler istisna.
- Tek bir araç ekosistem yaratır. Lean olmadan modern formal matematik olmazdı; modern AI matematik olmazdı. Bir kişinin uzun vadeli yatırımı alan tanımlar.
Bağlam
Lean için: [[lean-modern-formal-matematik-dili]]. AlphaProof için: [[alphaproof-ai-matematik-olimpiyatinda-gumus-madalyaya]]. Gowers için: [[tim-gowers-fields-madalyali-matematikcinin-ai-ile-bulusmasi]]. Microsoft Research için: [[bryan-catanzaro-nvidia-deep-learning-altyapisinin-mimari]] (büyük şirket araştırma). AI4Science için: [[ai-icin-bilim-protein-ilac-malzeme-yeni-aydinlanma]].
Etiketler
Kendinizi Test Edin
Cevaplarınız profilinizde istatistik olarak saklanır.
1. de Moura'nın akademik kökeni nedir?
2. Z3 nedir?
3. Lean ne zaman başladı?
4. Lean 4 ne ekledi?
5. de Moura 2023'te nereye geçti?
İlgili Yazılar
Brahmagupta: Sıfıra Kurallar Koyan ve Negatif Sayıları Borç Olarak Tanımlayan 7. Yüzyıl Hintlisi
628 yılında Brahmagupta, sıfırın aritmetiğini ve negatif sayıların kurallarını ilk kez sistematik biçimde yazdı. Borç-mülk metaforuyla negatif sayıları meşrulaştırdı, ikinci dereceden denklem formülünü genelleştirdi.
Bilim TarihiHypatia: İskenderiye'nin Son Büyük Kadın Matematikçisi ve Bir Çağın Sonu
M.S. 4. yüzyıl İskenderiye'sinde, dünyanın en büyük kütüphanesinin gölgesinde bir kadın geometri ve astronomi dersleri veriyordu. Hikâyesi, bir bilim insanının ötesinde, bir çağın bittiğini anlatır.
Bilim TarihiÉtienne Bézout: Fransız Donanmasının Matematik Hocası ve Adı Yanlış Yere Yapışmış Cebirci
Adı bugün her kriptografi dersinde geçen Bézout, hayatta sınava hazırlanan denizci adaylarına ders kitabı yazdı. Ünü, kendi bulmadığı bir teoremden geldi; kendi büyük teoremi ise nesiller boyunca anlaşılamadı.