Двое математиков русского происхождения из Ливерпуля, Алексей Лисица и Борис Конев, придумали интересную дилемму: что будет, если заставить компьютерную программу решить математическую задачу, но решение будет слишком сложным и длинным, чтобы его проверил человек?

Для примера учёные взяли так называемую Проблему несоответствия Эрдеша, сформулированную знаменитым венгерским математиком Полом Эрдешем (Paul Erdős). Задача построена вокруг поиска закономерности в бесконечном списке всего двух чисел «1» и "-1". Проблема возникает в тот момент, когда отсекается бесконечная последовательность, а затем создаётся конечная последовательность с использованием определённой константы. Сумма чисел и называется фигурой несоответствия.

Лисица и Конев ввели условия задачи с константой несоответствия «2» в компьютер со специальным программным обеспечение SAT-solvers («Решатели задач выполнимости булевых формул»), которые предназначены для создания математических доказательств.

Компьютер выдал файл с решением математической проблемы, объём которого превышал на пару гигабайтов объём всей «Википедии». Очевидно, что человеку проверить это решение будет не под силу. И потому учёные задают вопрос всем своим коллегам: готовы ли мы настолько доверять компьютерам, чтобы они самостоятельно решали математические и другие логические задачи?