ha már a kocsmatúra útvonalát is a terminátor optimalizálja majd

Szóval az ópenéjáj úgy tűnik, megpróbálta ellopni a startot a matematikai olimpián elért eredményük közlésével, közben kiderült, hogy a dípmájnd is ugyanolyan jól szerepelt (ugyanazokat a feladatokat oldották meg tökéletesen, de az ő eredményüket a szervezők certifikálták és állítólag a szervezők azt is kérték, hogy csak az olimpia vége után hét napra közöljék az eredményeket). Közben meg egy kínai csapat, a bájtdensz is ezüstöt ért el, de ők a lean nyelvben formalizált megoldást generáltak (az még nem világos, hogy a feladatok eredeti kiírását a rendszer fordította át lean formalizmusba, vagy azt emberekre bízták (ez utóbbira tippelnék, mert tudományosan maga a formális bizonyítás az érdekesebb, de persze az életben a természetes nyelvből automatikus formalizálás sem piskóta feladat)).

Szóval nagyon úgy tűnik, hogy ez a nemzetközi matematikai olimpia szintű feladatmegoldás lassan be lesz húzva, ami szerintem egy óriási lépés. A dípmájnd ígérte is, hogy nemsokára valamilyen formában elérhető lesz a rendszerük, gondolom fizetni kell majd érte, reméljük nem túl sokat. Én legalábbis úgy vagyok vele, hogy gyakran ütközöm matematikai problémákba munkám során (az informatikaiakkal jobban tudok küzdeni) és hát elég gyengécskén oldom meg őket, szerintem amikor a láthatóságon dolgoztam, nagyon jó lett volna, ha nem én kellett volna kódolás után megtaláljam azokat az ellenpéldákat amelyek invalidálták a megoldásomat, hanem mondjuk egy mesterséges intelligencia megmondta volna nekem, hogy ez bizony nem jó ötlet. De egyébként az élet is tele van matekfeladatokkal, csak az emberek próbálják nem észrevenni őket, hogy ne frusztrálja őket, hogy nem tudják megoldani. Erre én be fogok fizetni, ha havi 10 dollárból megúszom (nem is tudom hogy van a dzsemináj árazása, remélem van ilyen réteg). Ha még azt is megkapnánk, hogy formalizálja a rendszer a megoldást leanben és azt valahogy hozzá lehet fordítani a C++ programhoz, akkor aztán már tényleg itt lesz a kánaán. A tudományok fejlődésének komoly mérföldköve lesz ez (persze arra még várni kell, míg az a generáció, amely számítógéppel kezdi a matematikai modellezést átveszi a stafétát).

Demó.

Zene. 

AI.