Theorem proverlar g'oyasi kechagina paydo bo'lib qolgan narsa emas.

Man bilganim Automath project eng birinchi teorem proverlardan batafsil: https://automath.win.tue.nl/

Umuman olganda bu mavzular asosida juda ko'plab ishlar qilib kelinyabti. Theorem proverlar katta tarixga ega bo'lsada haligacha juda aktiv izlanishlar qilib kelinyotgan sohalardan.

Umuman olganda bu sohalar ham raqamli dunyoning bir ustuni desak bo'ladi. Mavzular atrofida juda ham ko'p qiziq tadqiqotlar mavjud. Hozirgacha SAT solverlar o'rtasida raqobat bor, kim tez ishlaydigan SAT solver qilishga musobaqalashadi: https://satcompetition.github.io/