Akademisyenler öncülüğünde matematik/fizik/bilgisayar bilimleri soru cevap platformu
0 beğenilme 0 beğenilmeme
264 kez görüntülendi

Belki duymussunuzdur Lean diye bir ispat asistani/programlama dili  var. Bu dili programlama gibi kullanmak da mumkun ama asil amaci ispatlarimizin dogrulugunu kontrol etmesi. Terrenca Tao yakin zamanda bir ispatini Lean de formalize ederken yaptigi ufak bir hatayi Leanin yakalamasindan bahsetmisti. Suan halihazirda lisan matematiginde ogrenilen onemli bazi teoremleri formalize etmisler Leande
Ben bu dile hafiften heves ettim. Soyle bir kaynak buldum. Burada uc tane oyun mevcut

  • Dogal sayilar oyunu
  • Kumeler teorisi oyunu
  • Mantik oyunu

Oyunlarda matematik birinci sinifta gordugumuz cesitli ispatlari yapiyoruz. Oyunlari oynarken universitede neden bazi matematik ispatlarimin yarim puan aldigini farkettim. (Iff in iki yonunu de kanitlamadan Lean memnun kalmiyor)
Bu oyunlar dili degil ama dilde kullanilan "taktik" leri anlatiyor.  (Taktikler ispat yazarken kullandigimiz "meta programlar")

Tam olarak dili anlatmasa da guzel bir giris oldugunu dusundum.
Ilgilenen olursa bu oyunlari burada soru olarak sormayi planliyorum.
Nasil sorariz bu oyunlari burada cok emin degilim ama onu da bu soruda tartisiriz   

Serbest kategorisinde (1.6k puan) tarafından  | 264 kez görüntülendi
Allah iyi Lean'i versin.
20,260 soru
21,785 cevap
73,460 yorum
2,350,647 kullanıcı