Článek se zabývá možnostmi využití počítačů v matematice a výuce matematiky, především v algebry. Představuje možnosti systémů pro automatické dokazování v predikátové logice prvního řádu.