Ова акција има за циљ јачање интероперабилности и употребљивости доказних система и омогућавању да формално доказивање теорема уђе у нову еру. По први пут окупља све програмере и кориснике система за доказивање теорема у Европи. Да би учинили доказе разменљивим, у заједничком логичком оквиру ће изразити логичке основе система за доказивање које користе и развијаће алате за међусобно превођење доказа развијених у појединачним системима у заједнички логички систем и за превођење доказа из заједничког логичког система у систем за доказе који користе.