Асисте́нт дове́дення теоре́м () або інструмент інтерактивного доведення теорем () — програмне забезпечення, яке дозволяє користувачам займатися математикою на комп'ютері, але не стільки обчисленнями (чисельними чи символьними), як визначеннями і доведеннями. За допомогою такої системи, користувач може формалізовано будувати математичну теорію на основі визначених аксіом та здійснювати логічні операції над визначеннями.
До пропонентів використання асистентів доведення теорем належать такі математики як Володимир Воєводський, Томас Гейлс та Кевін Баззард. Водночас, станом на 2021 рік, асистенти доведення теорем використовуються у передових математичних дослідженнях рідко.
Історія
У 2017 році в науковому журналі було опубліковане формалізоване доведення гіпотези Кеплера, виконане у системах HOL Light та Isabelle.
У 2021 році асистент Lean було використано для формалізації доведення нової теореми Петера Шольце в галузі , у доведенні якої він не був цілком упевнений. Формалізацію було здійснено групою волонтерів під керівництвом Йогана Коммеліна (Johan Commelin). Таким чином було показано, що система Lean може бути корисною у передовій математиці.
Список асистентів доведення теорем Agda Coq HOL Light Isabelle Lean Metamath
Примітки