Асисте́нт дове́дення теоре́м (англ.proof assistant)[1] або інструмент інтерактивного доведення теорем (англ.interactive theorem prover)[2] — програмне забезпечення, яке дозволяє користувачам займатися математикою на комп'ютері, але не стільки обчисленнями (чисельними чи символьними), як визначеннями і доведеннями. За допомогою такої системи, користувач може формалізовано будувати математичну теорію на основі визначених аксіом та здійснювати логічні операції над визначеннями.[1]
До пропонентів використання асистентів доведення теорем належать такі математики як Володимир Воєводський,[3][4]Томас Гейлс[5] та Кевін Баззард.[6] Водночас, станом на 2021 рік, асистенти доведення теорем використовуються у передових математичних дослідженнях рідко.[7]
У 2021 році асистент Lean було використано для формалізації доведення нової теореми Петера Шольце в галузі конденсованої математики[en], у доведенні якої він не був цілком упевнений. Формалізацію було здійснено групою волонтерів під керівництвом Йогана Коммеліна (Johan Commelin).[9][10] Таким чином було показано, що система Lean може бути корисною у передовій математиці.[9]