Доказательства с ошибками

Математическое доказательство — это алгоритмически проверяемое рассуждение; в контексте пропозициональной логики — рассуждение, проверяемое за полиномиальное время. Таким образом, система доказательств — это алгоритм; процедура поиска доказательств — тоже алгоритм.
Что будет, если разрешить этим алгоритмам изредка ошибаться? Это приводит к несколько иному понятию доказательства — эвристическому доказательству. Можно требовать от доказательств всё меньшей и меньшей вероятности ошибки, в конечном итоге получая доказательства только классических теорем (за счёт экспоненциальной длины доказательства и времени поиска). Для пропозициональных тавтологий существует процедура _оптимального_ поиска эвристических доказательств — в отличие от классического (неэвристического) случая, где существование такой процедуры является открытым вопросом, эквивалентным существованию оптимальной системы доказательств (имеющей самые короткие доказательства для каждой тавтологии).
Доклад основан на серии работ, совместных с Д.Ицыксоном, И.Монаховым, В.Николаенко, А.Смалем.