Асистент доведення теорем

Асисте́нт дове́дення теоре́м (англ. proof assistant)^[1] або інструмент інтерактивного доведення теорем (англ. interactive theorem prover)^[2] — програмне забезпечення, яке дозволяє користувачам займатися математикою на комп'ютері, але не стільки обчисленнями (чисельними чи символьними), як визначеннями і доведеннями. За допомогою такої системи, користувач може формалізовано будувати математичну теорію на основі визначених аксіом та здійснювати логічні операції над визначеннями.^[1]

До пропонентів використання асистентів доведення теорем належать такі математики як Володимир Воєводський,^[3][4] Томас Гейлс^[5] та Кевін Баззард.^[6] Водночас, станом на 2021 рік, асистенти доведення теорем використовуються у передових математичних дослідженнях рідко.^[7]

Історія

У 2017 році в науковому журналі було опубліковане формалізоване доведення гіпотези Кеплера, виконане у системах HOL Light та Isabelle.^[8]

У 2021 році асистент Lean було використано для формалізації доведення нової теореми Петера Шольце в галузі конденсованої математики^[en], у доведенні якої він не був цілком упевнений. Формалізацію було здійснено групою волонтерів під керівництвом Йогана Коммеліна (Johan Commelin).^[9][10] Таким чином було показано, що система Lean може бути корисною у передовій математиці.^[9]

Список асистентів доведення теорем

• Agda
• Coq
• HOL Light
• Isabelle
• Lean
• Metamath