Teoremlərin avtomatik sübutu (ing. Automated Theorem Proving, ATP, həmçinin Automated deduction) — isbat, proqram vasitəsilə həyata keçirilmişdir. Riyazi məntiqin aparatına əsaslanır. Süni intellekt nəzəriyyəsinin fikirlərindən istifadə olunur. İsbat prosesi təkliflərin məntiqi və predikatların məntiqinə əsaslanır.
Hətta olduqca sadə nəzəriyyələrin həllolunmazlığı səbəbindən yalnız yarı avtomatik insan maşın sübutları praktik tətbiq olunur. Üstəlik, tam avtomatlaşdırıldıqdan sonra sübut hesablama adlanır. Yalnız daha mürəkkəb nəzəriyyələrin sübutunu yoxlamaq üçün tam avtomatik ola bilər (bu üçün hazırlayırsınızsa).
Hal-hazırda, sənayedəki teoremlərin avtomatik sübutu, əsasən inteqrasiya edilmiş sxemlərin və proqramların işlənməsi və yoxlanılmasında istifadə olunur. Pentium prosessorlarında bölmə xətası aşkar edildikdən sonra müasir mikroprosessorların üzən nöqtə əməliyyatlarının mürəkkəb modulları çox diqqətlə hazırlanır. AMD, Intel və digər şirkətlərin yeni prosessorları bölünmə və digər əməliyyatların düzgün aparıldığını yoxlamaq üçün teoremlərin avtomatik sübutundan istifadə edirlər.
Microsoft Windows 7 əməliyyat sisteminin kodunu və digər proqram məhsullarını yoxlamaq üçün Z3 teoreminin avtomatik sübutundan istifadə edir[1].