Takie dowody wzbudzają kontrowersje, gdyż niemożliwe jest zweryfikowanie ich przez człowieka. Innym przykładem użycia komputerów jest rozproszony projekt Seventeen or Bust sprawdzający potencjalnych kandydatów na liczby Sierpińskiego. Dowód niezależności to dowód, że pewnego zdania nie można udowodnić. Przykładem jest dowód niezależności hipotezy continuum, wykorzystujący forsing. Dowód konstruktywny to dowód polegający na znalezieniu pewnego obiektu spełniającego wymagane założenia. Przykład: aby udowodnić, że wielomian ma pierwiastek rzeczywisty, wystarczy zauważyć, że jest nim liczba 2. Aby udowodnić, że każdy graf spójny zawierający co najwyżej dwa wierzchołki stopnia nieparzystego ma drogę Eulera, można podać algorytm znajdujący ją. Dowód niekonstruktywny to dowód polegający na wykazaniu, że istnieje obiekt spełniający założenia, jednak bez konstrukcji. Przykład: aby udowodnić, że wielomian ma pierwiastek rzeczywisty, zauważmy, że przyjmuje on wartość ujemną dla i dodatnią dla Ponieważ jest funkcją ciągłą, z twierdzenia Cauchy’ego wynika, że wielomian ma miejsce zerowe w przedziale Innym przykładem jest wykorzystanie zasady szufladkowej Dirichleta. Dowód nieefektywny to dowód wykorzystujący aksjomat wyboru.
W złożonych, wielostopniowych dowodach wykorzystuje się twierdzenia pomocnicze, tzw.