Európa vezető felfedező kutatásai között az ELTE projektje
Az Európai Kutatási Tanács (European Research Council, ERC) a Horizont Európa keretprogramban a felfedező kutatásoktól a hasznosítás kezdeti fázisáig díjazza a legígéretesebb kutatásokat. A Consolidator Grant pályázaton a már kutatócsoporttal és kiemelkedő eredményekkel rendelkező, tudományos áttörés ígéretét hordozó kutatásokat ismerik el.
Kaposi Ambrus és csapata Higher Observational Type Theory (HOTT / Magasabb megfigyelés-alapú típuselmélet) című kutatásával
a számítógépes bizonyítórendszerek használatát forradalmasíthatja.
A számítógépes bizonyítórendszerek a típuselméletre (type theory) épülnek. A típuselmélet mind a matematikusok, mind pedig az informatikusok bizonyítási és helyességellenőrzési problémáira megoldást kínál, hiszen olyan formális nyelvi eszközt ad a kezünkbe, amellyel egyszerre lehet programokat és matematikai bizonyításokat írni. Egy program típusa maga az állítás, a típusnak megfelelő program pedig az állítás bizonyítása.
A típuselmélet magasabb-dimenziós modelljeiben a típusok elemeit absztrakt terek pontjaival, az egyenlőség típust pedig a pontok közötti utakkal adják meg. Ilyen modellekre építve fejlesztették ki a homotópia-típuselméletet (homotopy type theory), amelyben teljesül az izomorf típusok egyenlőségének elve. Ezzel az elvvel a számítógépes bizonyítás közel kerül a mindennapos matematikusi gyakorlathoz, ahol az izomorf struktúrákat azonosnak tekintik.
A HOTT projekt célja a homotópia-típuselmélet egy új változatának kidolgozása, amelyben a magasabb-dimenziós geometria nem kézzel van beépítve, hanem emergens. Az alapötlet, hogy az egyenlőség típus nem geometriai módon, hanem számítással van megadva. A megoldás a homotópia-típuselméletet elmagyarázhatóvá teszi, és a bizonyításokat rövidíti, hiszen a bizonyítások egyes részei automatikus számításokká válnak. Az új típuselmélet hosszú távon hozzá fog járulni a matematikai bizonyítások számítógépes ellenőrzésének és a szoftverek helyességbizonyításának fejlődéséhez azáltal, hogy lehetővé teszi az absztrakt, újra felhasználható bizonyítások készítését.
További ELTE-s projektek a Horizont Európa program támogatásával
