A bizonyításasszisztens szoftverek (Coq, Lean) használata nem csak a strukturális bizonyításelmélészek hóbortja, nagyon hasznosan alkalmazhatja bárki, akinek elég ideje és motivációja van. Fontos tudni azonban, hogy a bizonyításasszisztensek nem a jól ismert halmazelméleti gondolatokat követik, hanem egy másik logikai világból származnak a fogalmaik, éspedig a függő típuselméletből. Ahhoz tehát, hogy értsük, hogyan zajlik a bizonyításasszisztensek működése legalább az egyszerű (nem függő) típuselmélettel (STT) meg kell ismerkednünk. Az előadásban az STT elméletével és egy szemantikájával, a kartéziánusan zárt kategóriákkal (CCC) ismerkedünk meg, és Coq-ban leprogramozott eredményeket és részeredményeket láthatunk a CCC helyességével és teljességével kapcsolatban. Az előadás végén bemutatok egy-két példát arra is, hogy a Lean-t hogyan lehet hétköznapi matematikai állítások bizonyítására használni.