Доказательство: как вы знаете, а не насколько вероятно

Множества, булева алгебра и Big-O держатся на одном действии, которое вы до сих пор делали молча: проверить несколько случаев и решить, что закономерность сохранится. Для множества из двух элементов это нормально — вы видите всё. Для утверждения про каждое целое число это неверно, и вся разница между профессионалом и новичком прячется именно в этом зазоре. Доказательство — не более сильная проверка. Это объект другого рода: конечное рассуждение, которое накрывает бесконечно много случаев сразу.

Сначала прочитайте утверждение внимательно: большинство плохих доказательств бьют не по тому предложению, которое написано на доске. Утверждение «для каждого целого n» по определению не допускает исключений, а утверждение «существует n» просит предъявить один пример. Это противоположные стратегии. Утверждение ниже выглядит превосходно. Запустите его — оно держится сорок значений подряд, то есть куда лучше, чем большинство закономерностей, которым вы доверяли.

claim: for every integer n >= 1,  n^2 + n + 41  is prime

n = 1    43         prime
n = 2    47         prime
n = 3    53         prime
n = 4    61         prime
n = 5    71         prime
n = 10   151        prime
n = 20   461        prime
n = 39   1601       prime
n = 40   1681 = 41 * 41   composite

confirmed: 39 cases before that one

При n = 40 значение распадается в произведение. Этот единственный случай — полное и окончательное опровержение, и стоит он одной строки. Такая асимметрия — самое полезное в этом уроке: чтобы доказать универсальное утверждение, нужно рассуждать сразу обо всех случаях, а чтобы разрушить его, достаточно одного. Заметьте также, чего стоили сорок успехов, — ничего. Это были не слабые свидетельства в пользу утверждения, а вообще не свидетельства: утверждение было ложным всё это время. Когда ищете контрпример, ищите по краям: n = 0, n = 1, отрицательные числа, пустой список, наибольшее значение, которое вмещает ваш тип. Большинство ложных универсальных утверждений о коде умирает на граничном случае, а не в середине.

Прямое доказательство — обычное: начинаете с определений и приходите к утверждению, не принимая ничего недоказанного. Когда рассуждение в разных ситуациях устроено по-разному, разбейте его на случаи и проверьте, что случаи покрывают всё. Утверждение ниже доказывается в две строки, но доказательством это делает только последняя строка: она утверждает, что каждое целое попадает в один из двух случаев. Без неё вы показали два примера, а не теорему.

claim: for every integer n,  n^2 + n  is even

n^2 + n  =  n * (n + 1)

case A:  n = 2k       ->  n * (n + 1) = 2 * k * (n + 1)
case B:  n + 1 = 2k   ->  n * (n + 1) = 2 * k * n

int(n) = A union B

Доказательство от противного нужно для утверждений, которые трудно атаковать в лоб, — обычно это утверждения о несуществовании. Вы предполагаете противоположное и идёте по следствиям, пока два факта не перестанут уживаться вместе. Классический пример ниже. Каждый шаг — обычная алгебра плюс один арифметический факт: если квадрат a чётен, то и a чётно. Противоречие здесь не в том, что случилось что-то неожиданное, а в том, что результат бьёт по исходному предположению: у a и b не было общего множителя.

claim: no integers a, b with  sqrt(2) = a / b

assume integers a, b exist, gcd(a, b) = 1

  a / b   = sqrt(2)
  a^2     = 2 * b^2
  a^2 even              ->  a = 2k
  4 * k^2 = 2 * b^2
  b^2     = 2 * k^2     ->  b = 2m
  gcd(a, b) >= 2  ->  contradicts gcd(a, b) = 1

assumption false

Именно тут умирает большинство неудачных доказательств от противного, и тупик стоит назвать, чтобы вы его узнавали. Если предположение было слабым, полученное противоречие может означать лишь то, что предположение неудобно, а не то, что оно ложно. Если предположить дробь с общим множителем, противоречия не возникло бы вовсе. Лекарство не в том, чтобы сильнее давить на алгебру, а в том, чтобы вернуться и предположить самую сильную и конкретную версию противоположного. Доказательство от противного ровно настолько хорошо, насколько сильно предположение, которое оно убивает.

Так чего же стоит тест? Очень многого, но он не доказательство и не станет им, если добавить ещё тестов. Свидетельства повышают уверенность, доказательство закрывает вопрос. Настоящей инженерии нужно и то и другое, и путаница между ними — это как раз то, из-за чего в прод уезжают утверждения, которые никто на самом деле не проверял. Честная позиция узкая и полезная: моё доказательство показывает, что алгоритм возвращает отсортированный массив, а мои тесты показывают, что он укладывается в ту память, которая у нас есть. Ни одно из этих предложений не выдаёт себя за другое.