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

Асисте́нт дове́дення теоре́м (англ. 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]

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

[ред. | ред. код]

Примітки

[ред. | ред. код]
  1. ↑ а б Geuvers, Herman (February 2009). Proof assistants: History, ideas and future. Sādhanā. 34 (1): 3—25. doi:10.1007/s12046-009-0001-5. S2CID 14827467.
  2. ↑ Moura, Leonardo de; llrich, Sebastian. The Lean 4 Theorem Prover and Programming Language (PDF). Automated Deduction–CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings 28. Springer International Publishing: 625—635.
  3. ↑ Hartnett, Kevin (19 травня 2015). Will Computers Redefine the Roots of Math?. Quanta Magazine.
  4. ↑ Voevodsky, Vladimir (Summer 2014). The Origins and Motivations of Univalent Foundations: A Personal Mission to Develop Computer Proof Verification to Avoid Mathematical Mistakes (PDF). The Institute Letter. Institute for Advanced Study: 8—9.
  5. ↑ Hales, Thomas (18 вересня 2018). A Review of the Lean Theorem Prover. Процитовано 6 жовтня 2020.
  6. ↑ Buzzard, Kevin. The Future of Mathematics? (PDF). Процитовано 6 жовтня 2020.
  7. ↑ Hartnett, Kevin (28 липня 2021). Proof Assistant Makes Jump to Big-League Math. Quanta Magazine.
  8. ↑ Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland (29 травня 2017). A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi. 5: e2. doi:10.1017/fmp.2017.1.
  9. ↑ а б Hartnett, Kevin (28 липня 2021). Proof Assistant Makes Jump to Big-League Math. Quanta Magazine.
  10. ↑ Commelin, Johan (2022). Liquid Tensor Experiment (PDF). Mitteilungen der Deutschen Mathematiker-Vereinigung. 30 (3): 166—170. doi:10.1515/dmvm-2022-0058.