Európa élvonalbeli felfedező kutatásai közé tartozik az ELTE által irányított projekt, amely új dimenziókat nyit a tudományos világban.

Kaposi Ambrus 2024-ben Magyarországról egyedülálló módon nyerte el az ERC Consolidator Grant támogatást, amely a legkiválóbb európai tudományos pályázatok közé tartozik. Az élettelen természettudományok és műszaki tudományok kategóriájában összesen 928 pályázatot nyújtottak be, és ő a kiválasztott 131 közé került. Ez a siker nemcsak a kutatásának elismerése, hanem a magyar tudományos közösség számára is jelentős mérföldkő.

Az Európai Kutatási Tanács (European Research Council, ERC) a Horizont Európa keretprogram keretein belül a felfedező kutatásoktól a hasznosítás korai szakaszáig terjedő spektrumon támogatja a legígéretesebb tudományos projekteket. A Consolidator Grant pályázat célja, hogy elismerje azokat a kutatásokat, amelyek már meglévő kutatócsoportokkal és figyelemre méltó eredményekkel rendelkeznek, és amelyek tudományos áttörést ígérnek a jövőben.

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 alkalmazása új dimenziókat nyithat meg, forradalmi változásokat idézve elő a területen.

A számítógépes bizonyítórendszerek alapját a típuselmélet képezi, amely nem csupán a matematikai gondolkodás, hanem az informatikai problémák megoldásában is kulcsszerepet játszik. A típuselmélet egy formális nyelvet biztosít, amely lehetővé teszi számunkra, hogy párhuzamosan foglalkozzunk programozással és matematikai bizonyítások készítésével. Ezen a téren a programok típusa egyben állítást is jelent, míg a típusnak megfelelő programot bizonyítékként értelmezhetjük az adott állításra.

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.