Egyedüli magyar résztvevőként az ELTE kutatója lenyűgöző, több mint 780 millió forintnyi pályázati támogatást szerzett.

Kaposi Ambrus típuselméleti kutatása jelentős elismerésben részesült, hiszen az Európai Kutatási Tanács (ERC) Consolidator Grant pályázatán 1,9 millió eurós, körülbelül 781 millió forintnak megfelelő támogatást nyert el. Ezt a hírt kedden jelentette be az Eötvös Loránd Tudományegyetem (ELTE).

A 2024-es évben Magyarországon egyedülálló módon, a kutató elnyerte az ERC pályázati támogatását.

A kutatási területen, amely az élettelen természettudományok és a műszaki tudományok világát öleli fel, összesen 928 pályázat érkezett be. Ebből a szigorú válogatáson 131 pályázat nyert el helyet a legjobbak között.

Az ERC a Horizon Europe keretprogram keretein belül a legígéretesebb kutatások elismerésére fókuszál, kezdve a felfedező kutatásoktól egészen a hasznosítás kezdeti szakaszáig. A Consolidator Grant pályázat célja, hogy támogassa azokat a kutatócsoportokat, amelyek már bizonyították eredményeik jelentőségét, és tudományos áttörés ígéretét hordozzák. Különösen figyelemre méltó Kaposi Ambrus és csapata, akik a Magasabb megfigyelés-alapú típuselmélet (Higher Observational Type Theory - HOTT) című kutatásukkal a számítógépes bizonyítórendszerek alkalmazását forradalmasíthatják - hangsúlyozták a szakértők.

Az MTI által közzétett információk alapján a számítógépes bizonyítórendszerek alapjául a típuselmélet szolgál. Ez a megközelítés a matematikai és informatikai területeken egyaránt választ ad a bizonyítási és helyességellenőrzési kihívásokra. A típuselmélet olyan formális nyelvi eszközöket biztosít a felhasználók számára, amelyek lehetővé teszik, hogy párhuzamosan dolgozzanak programok és matematikai bizonyítások létrehozásán.

- kifejtették.

A típuselmélet magasabb dimenziós modelljeiben a típusok elemei absztrakt terek pontjaiként jelennek meg, míg az egyenlőség típusa az egyes pontok közötti utakat reprezentálja. Ezen alapokra építve alakították ki a homotópia-típuselméletet (homotopy type theory), amelyben érvényesül az izomorf típusok egyenlőségének elve. Ez az elv lehetővé teszi, hogy a számítógépes bizonyítások egyre inkább közelítsenek a matematikai gyakorlat hagyományos módszereihez, ahol az izomorf struktúrákat azonosnak tekintik - ahogyan azt a szakértők is kifejtették.

A HOTT-projekt keretében egy innovatív homotópia-típuselmélet kifejlesztése a cél, amelyben a magasabb dimenziós geometria nem csupán kézi beavatkozással, hanem emergens módon jelenik meg. Az alapgondolat az, hogy az egyenlőség típusát nem geometriai eszközökkel, hanem számítási módszerekkel definiálják. Ez a megközelítés lehetővé teszi a homotópia-típuselmélet mélyebb megértését, valamint jelentősen egyszerűsíti a bizonyítási folyamatokat, mivel a bizonyítások egyes szakaszai automatikusan generált számításokká alakulnak.

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

Tedd különlegessé a szövegedet azzal, hogy lehetővé teszi az absztrakt és újrahasznosítható bizonyítások megalkotását.