Tak, są.

Na przykład w 1976 roku dwóch matematyków udowodniło twierdzenie o 4-kolorowalności grafów planarnych. Tyle, że przeprowadzili oni skomplikowane rozumowanie w wyniku którego dowiedli, że jeśli kilka tysięcy konkretnych grafów planarnych są 4-kolorowalne, to wszystkie grafy planarne są 4-kolorowalne. Ponieważ tych grafów było za dużo do przerobienia przez człowieka, napisali oni program komputerowy który sprawdził te kilka tysięcy konkretnych grafów. I to w latach 70-80-tych wielu matematykom się nie spodobało.

Co ciekawe, przez kilkadziesiąt lat uproszczono ich dowód, ale do dzisiaj nie ma dowodu tego twierdzenia który nie korzystałby z pomocy komputera.