Terence Tao, QED Mantık Oyununu Bir Coding Agent ile Lean Grimoire Olarak Yeniden İnşa Etti

Ne oldu

Matematikçi Terence Tao, etkileşimli bir mantık ders kitabının yeniden inşa edilmiş bir sürümünü yayımladı; proje şu an Lean Grimoire çalışma adını taşıyor ve Tao oyun testçileri arıyor. Tao, 11 Kasım tarihli ve ertesi gün Hacker News'in ana sayfasına ulaşan blog yazısında, projeyi modern bir coding agent yardımıyla yeniden inşa ettiğini ve oyunu mantık kanıtlarını öğretmek ile Lean proof assistant öğrenmek için yararlı kılacak özellikler eklediğini söylüyor.

QED'den Lean Grimoire'a

Uygulama, Tao'nun 2018'de özgün olarak inşa ettiği ve o dönemde blogunda duyurduğu JavaScript tabanlı etkileşimli ders kitabı QED'nin modernleştirilmiş hâli. QED, önerme mantığını ve birinci dereceden mantığı bir zanaat oyunu biçiminde öğretiyordu: Oyuncu, verilen bir hipotez kümesinden yola çıkarak mantık kurallarını uygulıyor ve hedef bir sonuca ulaşıncaya kadar ilerliyordu.

Tao, coding agent'larla matematiksel görselleştirme uygulamacıkları geliştirme denemelerine Temmuz ayında başladığını, ancak yoğun geçen birkaç ayın bu projeleri bir kenara bırakmasını gerektirdiğini yazıyor. Yakın zamanda bu projelerden birine dönecek zaman buldu ve yeniden inşa edilen oyun bunun sonucu.

Yeniden inşa neler ekliyor

İki ek öne çıkıyor. İlki, oyuncunun mevcut oyun durumuna ilişkin sürmekte olan bir Lean kanıtını gösterme seçeneği; böylece oyunda yapılan hamleler, bir proof assistant'ın izleyebileceği bir kanıtın adımlarına karşılık geliyor. İkincisi, oyunu fantastik temalı süsleme metinleriyle donatan şakacı bir fantastik mod; bu modda matematiksel ifadeler iksirler, matematiksel ifadeler de tomarlar olarak görünüyor.

Yazıda Tao'nun hangi coding agent'ı kullandığı ya da uygulamanın ne kadarını agent'ın üstlendiği belirtilmiyor; yalnızca yeniden inşanın bir agent ile gerçekleştirildiği söyleniyor.

Oyun testçilerine açık çağrı

Tao yazıyı, okurlardan uygulamayı test etmelerini isteyerek bitiriyor; belirtilen hedef, onu mantık kanıtlarını ve Lean'i öğretme aracı olarak daha yararlı hâle getirmek. Hacker News'teki yer edinme, bu isteği büyük bir teknik kullanıcı kitlesinin önüne çıkarıyor; bu kitle, hem oyunu baskı testine sokmaya hem de Lean entegrasyonu konusunda anlamlı geri bildirim vermeye en elverişli grup.

Neden önemli

Lean Grimoire mütevazı bir proje, ancak güncel üç akışın kesişim noktasında duruyor.

Bu, bir araştırma matematikçisinin agentic coding araçlarını kullanarak çalışan bir yazılım çıkardığının somut, adı konmuş bir örneği. Tao, agent'ı, aksi hâlde zaman ayıramayacağı sekiz yıllık bir yan projeyi canlandırmasını sağlayan şey olarak tanımlıyor; bu da tam olarak bu araçların açığa çıkaracağı öne sürülen uykuya dalıp değerini koruyan türden iş.

Ayrıca iki kitle arasında köprü kurmaya çalışıyor: Oyun aracılığıyla biçimsel mantık öğrenenler ve matematiksel formalizasyonda giderek artan bir rol oynayan bir proof assistant olan Lean'i öğrenenler. Lean kanıtını oyun durumunun yanında göstermek, öğrenicilere sezgisel kural uygulamasından makine tarafından doğrulanan kanıta görünür bir yol sunuyor; proof assistant'ı ayrı ve daha dik bir beceri olarak ele almıyor.

Son olarak, topluluk tepkisi hikâyenin bir parçası. Hacker News ana sayfasında görünmek, bunun gibi niş araçların testçi ve katkıcı bulma biçimi ve Tao açıkça her ikisini de istiyor.