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