PCP теорема говорить, що для деякої універсальної константи K, для довільного n, всяке математичне доведення довжини n може бути переписано як інше доведення довжини poly(n), що може бути формально перевірене з 99% точністю ймовірнісним алгоритмом, що переглядає тільки K символів з цього доведення.
Альтернативне формулювання PCP теореми стверджує, що найбільша частка виконуваних обмежень задачі виконуваності обмежень є NP-важкою для наближення з константною точністю.
Формально, для деякої константи K і α < 1, наступна задача обіцяння (Lтак, Lні) є NP-важкою задачею розпізнавання:
Lтак = {Φ: всі обмеження у Φ є одночасно виконуваними}
Lні = {Φ: кожний розв’язок виконує менше ніж частку α обмежень Φ},
PCP теорема є кульмінацією тривалого часу роботи над інтерактивними та ймовірнісно перевірюваними доведеннями. Першою теоремою, що пов’язує стандартні доведення та ймовірнісно перевірювані доведення є твердження, що NEXP ⊆ PCP[poly(n), poly(n)], доведене Babai, Fortnow та Lund, (1990).
Після цього, метод, використаний у цій роботі, було розширено Бабаєм, Фортноу, Левіним та Шеґеді у 1991 (Babai та ін., 1991),
Файґе, Ґолдвасер, Лундом, Сафрою та Шеґеді (1991), і Аророю та Сафрою у 1992 (Arora та Safra, 1998), що дало змогу довести PCP теорему Аророю, Лундом, Мотвані, Суданом та Шеґеді у 1992 році (Arora та ін., 1998).
Babai, László; Fortnow, Lance; Lund, Carsten (1990), Nondeterministic exponential time has two-prover interactive protocols, SFCS '90: Proceedings of the 31st Annual Symposium on Foundations of Computer Science, IEEE Computer Society, с. 16—25, ISBN978-0-8186-2082-9.
Dinur, Irit (2007), The PCP theorem by gap amplification, Journal of the ACM, 54 (3): 12, doi:10.1145/1236457.1236459.