Tecniche di dimostrazione automatica e interattiva di teoremi al compute per problemi di geometria, algebra, analisi reale e complessa.