Nya teorier för datorverifiering

Axel Ljungström som ska disputera i matematik vid Stockholms universitet 2025, har tack vare ett anslag från Knut och Alice Wallenbergs Stiftelse erhållit en postdoktoral tjänst hos professor Ulrik Buchholtz, University of Nottingham, Storbritannien.

Ju mer sofistikerad matematik desto svårare blir det att finna fel i den matematiska bevisföringen. Ett sätt att göra bevisen pålitligare är att verifiera dem med hjälp av ett datorprogram, en bevisassistent. Målet för projektet är att utveckla teorier som ligger till grund för moderna bevisassistenter. I synnerhet handlar det om att kunna använda bevisassistenter för homotopiteori som är en del av den algebraiska topologin. 

För att få datorn att förstå homotopiteorins abstrakta matematik krävs ett nytt språk. Många av dagens bevisassistenter bygger på typteorier, en samling logiska system utvecklade för att utgöra grunden för all matematik. En av de viktigaste moderna typteorierna konstruerades på 1970-talet av Per Martin-Löf, i dag professor emeritus i logik vid Stockholms universitet. Så småningom har ett helt nytt matematiskt system vuxit fram – homotopi-typteori (HoTT). Det är skräddarsytt för att datorverifiera bevis från homotopiteorin. 

Homotopi-typteorin är ett matematiskt system med sina egna spelregler. Ofta krävs det att ny matematik uppfinns för att över huvud taget kunna uttrycka den klassiska homotopiteorin i andra termer. Nästa steg i projektet är att undersöka huruvida algoritmer kan användas för att genomföra datorverifieringen. På så sätt kan bevisföringen drastiskt förenklas även för matematiska satser som inte verkar vara beräkningsbaserade till sin natur. 

Foto: Elias Tingström