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
Kuantum Zeno Etkisi: Sürekli Baktığınız Bir Atom Neden “Donar”?
“İzlenen tencere kaynamaz” derler. Kuantum dünyasında bu söz şaşırtıcı biçimde gerçektir: bir parçacığı yeterince sık gözlemlerseniz, değişmesini fiilen durdurabilirsiniz. Antik bir paradoksun adını taşıyan bu etki neyi anlatır?
Bilim TarihiCasimir Etkisi: Boşluğun Bir İtme Kuvveti Var mı? Ve “1+2+3+… = -1/12” Gizemi
İki metal levhayı boşlukta yan yana koyun; hiçbir şey olmaması gerekirken birbirlerine doğru itilirler. Bu tuhaf kuvvetin ardında, sonsuz bir toplamı garip bir biçimde “evcilleştiren” bir matematik yatıyor.
Bilim TarihiDünyayı Sessizce Değiştiren Beş Fizik Denklemi
Bazı denklemler bir kâğıda sığar ama medeniyeti baştan yazar. İşte uçaktan GPS’e, internetten enerjiye kadar hayatımızı kuran beş denklem ve her birinin ardındaki sade fikir.