Математическое доказательство

Доказательства используют логику, выраженную математическими символами и естественный язык, который обычно допускает некоторую неоднозначность. В большинстве математической литературы доказательства пишутся на строгом неформальном языке. Чисто формальные доказательства, записанные полностью на символическом языке без использования естественного языка, рассматриваются в теории доказательств. Различие между формальными и неформальными доказательствами привело к многочисленным исследованиям современной и исторической математической практики, квазиэмпиризма в математике и так называемого математического фольклора — устной традиции в профессиональном математическом сообществе или в других культурах. Философия математики занимается ролью языка и логики в доказательствах и математикой как языком.

Можно утверждать, что понятие строгого математического доказательства — это то, что существенно отличает математику от других научных дисциплин^[3]. Математическое доказательство, в отличие от доказательств в других сферах человеческой деятельности (например, в праве, естественных науках и др.), по крайней мере принципиально неоспоримо^[4]. Не исключено, что удастся математически доказать , которое на самом деле неверно. Однако доказательство такого утверждения обязательно будет ошибочным, и эта ошибка должна быть (при достаточно тщательном рассмотрении) обнаружена. Источником ошибок при математическом доказательстве является не само понятие доказательства, а всегда и только ошибающиеся люди.

Во всех научных дисциплинах, кроме математики, теории оцениваются по степени соответствия реальному миру и по тому, насколько точно они объясняют и предсказывают реальные явления. Новые теории строятся так, чтобы соответствовать экспериментально установленным данным. Если они согласуются с этими данными, их признают верными. Если со временем выдвигается гипотеза, истинность которой существующая теория не может определить, проводится эксперимент, по результатам которого гипотеза либо отвергается, либо включается в признанную теорию. Если позже появляются экспериментальные данные, противоречащие существующей теории, эта теория отвергается и заменяется новой. Такой способ проверки гипотез и построения теорий называется индуктивным^[4].

Примером индуктивного доказательства может служить обоснование утверждения: «Завтра утром взойдёт Солнце». Из опыта нашего и наших предков мы знаем, что солнце всходило уже много тысяч раз. У нас нет никаких сведений о том, чтобы когда-либо утром солнце не взошло. Кроме того, солнце в последнее время не проявляет никаких необычных признаков, которые бы указывали на то, что с ним что-то не так, как когда-либо в известной истории. На основании этих фактов мы заключаем, что с пренебрежимо малой вероятностью ошибки солнце завтра утром снова взойдёт.

Однако индуктивное доказательство может быть весьма обманчивым. Например, в классической механике принимается за истинное утверждение, известное как Второй закон Ньютона, гласящее: «Если на тело действует сила, то тело движется с ускорением, прямо пропорциональным действующей силе и обратно пропорциональным массе тела». Это утверждение до второй половины XIX века соответствовало всем проводимым экспериментам и потому считалось истинным — индуктивно доказанным. Однако на рубеже XIX и XX века некоторые эксперименты показали, что движение света не подчиняется законам Ньютона, и это утверждение вместе со всей классической механикой было отвергнуто и заменено теорией относительности. Согласно этой теории, сила, действующая на тело, движущееся со скоростью, близкой к скорости света, вызывает лишь минимальное ускорение, а остальная вложенная энергия приводит к увеличению массы тела.

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

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

Все виды математических доказательств, начиная с исторических истоков этого понятия в Древней Греции и до настоящего времени, через всё многообразие различных методов доказательства, являются дедуктивными^[5].

Рассмотрим : «Произведение любых двух нечётных натуральных чисел — нечётное натуральное число».

Если проверить несколько малых натуральных чисел, увидим, что для них утверждение выполняется: 1 · 1 = 1, 1 · 3 = 3, 3 · 1 = 3, 3 · 3 = 9, 3 · 5 = 15 и т. д. Аналогично, например, с помощью компьютера можно проверить, что утверждение выполняется для всех чисел меньше 1 000 000; если этого недостаточно, можно увеличить границу сколь угодно высоко, например до 10^{1 000 000} (число, начинающееся с единицы, за которой следуют 1 000 000 нулей), и всегда обнаружим, что утверждение выполняется. После некоторого количества таких увеличений границы можно признать, что мы проверили достаточно примеров, чтобы быть почти полностью уверенными в правильности утверждения. Таким образом, утверждение доказано индуктивно. Однако мы никогда не можем быть полностью уверены, что какой-либо контрпример не находится сразу за числом, на котором мы остановили проверку (это называется проблемой горизонта).

В отличие от этого, дедуктивное доказательство следующее. Если m — нечётное число, то m − 1 — чётное число, то есть существует целое число k такое, что m − 1 = 2 · k. Для k достаточно взять (m − 1) / 2, что является целым числом благодаря чётности m − 1. Тогда m = 2 · k + 1. Аналогично, если n нечётное, существует целое число l, что n = 2 · l + 1. Тогда произведение m · n равно (2 · k + 1) · (2 · l + 1) = 4 · k · l + 2 · k + 2 · l + 1. Поскольку 4 · k · l + 2 · k + 2 · l очевидно чётно, то m · n нечётно, что и требовалось доказать. Теперь мы можем быть полностью уверены, что утверждение верно: для любых двух нечётных чисел каждый шаг доказательства выполняется, а значит, и его вывод.

Гипотеза о простых близнецах — это до сих пор (июль 2011) недоказанное утверждение из теории чисел, согласно которому существует бесконечно много простых чисел p таких, что и p + 2 — простое число. Пары таких чисел (p, p + 2) называются простыми близнецами.

Наибольшая из известных на данный момент пар простых близнецов — (65 516 468 355·2^{333 333} − 1; 65 516 468 355·2^{333 333} + 1), оба числа в этой паре имеют (в десятичной системе) 100 355 цифр^[6]. Несмотря на то, что известны столь большие примеры простых близнецов, нельзя считать гипотезу дедуктивно (математически) доказанной, поскольку возможно, что ни одной большей пары простых близнецов больше не существует — просто потому, что их нет. Тем не менее считается (и не только по причине приведённого индуктивного доказательства), что утверждение верно. Его доказательство остаётся одной из самых сложных проблем современной теории чисел^[7].

Согласно , в любой достаточно сложной (такой, чтобы в ней можно было говорить о натуральных числах) математической теории, аксиомы которой можно эффективно перечислить, существуют утверждения, которые в этой теории нельзя ни доказать, ни опровергнуть (такая теория называется неполной). К таким теориям относятся, например, Арифметика Пеано или Теория множеств Цермело — Френкеля.

Эти теоремы показывают, что дедуктивный способ доказательства в значительной степени ограничен. Невозможно дедуктивно доказать или опровергнуть все утверждения, которые верны даже в столь простой и доступной области, как натуральные числа.

От древних египтян и вавилонян не сохранилось ни одного математического доказательства в современном смысле слова. Сохранилось множество записей, фиксирующих решения различных конкретных задач и проблем. Считается, что эти задачи были уже достаточно абстрактны, а решения столь изящны, что за ними стояло глубокое понимание соответствующей области, включающее неявные доказательства правильности используемых методов^[5].

В Китае V — III век до н. э. наряду с практической математикой развивалась и логика. Ею занималась, в частности, школа последователей философа Мо-цзы, представители которой занимались теорией познания и логически доказывали свои утверждения^[8]. Одним из наиболее известных последователей Мо-цзы был Гунсунь Лун, живший в первой половине III века до н. э.

Однако логическое доказательство в Китае не получило дальнейшего развития. Учение Мо-цзы было полностью вытеснено ханьской династией конфуцианством, и позднейшие китайские философы к нему уже не возвращались.

Понятие дедуктивного математического доказательства возникло в Древней Греции^[5]. Как и вся тогдашняя математика, математическое доказательство было тесно связано с геометрией. Самые ранние математические доказательства относятся именно к этому времени — они сохранились в тринадцатитомном труде Евклида «Начала».

Математическое доказательство в современном смысле слова берёт начало в греческой геометрии, развивавшейся под влиянием философии Платона. Под влиянием этой философии геометры стремились постичь мир геометрических идей и созерцать содержащуюся в нём истину. В этом понимании математического доказательства в современном смысле ещё не существовало. Единственным способом с полной уверенностью узнать истину о геометрическом мире было непосредственно её созерцать — «очевидеть» её. Если геометру удавалось «очевидеть» истинность, например, теоремы Пифагора — то есть на мгновение действительно увидеть, что сумма площадей двух квадратов на катетах прямоугольного треугольника равна площади квадрата на гипотенузе, — это было только на то время, пока длилось его сосредоточение. Как только внимание ослабевало, взгляд, направленный в мир геометрических идей, затуманивался, и очевидность терялась. Чтобы вновь обрести эту очевидность и дать такую возможность другим математикам, геометр записывал инструкцию, как следует действовать (то есть на какие части геометрического мира смотреть), чтобы вновь увидеть истинность теоремы Пифагора. Такие инструкции, из которых позднее (в аристотелевском понимании геометрии) развились геометрические построения, были древнейшими предшественниками математических доказательств.

Платоновское понимание математики оказалось неустойчивым. По мере развития геометрии новые истины оказывались всё глубже скрытыми в мире геометрических идей. Геометру, желавшему «очевидеть» истину, приходилось прилагать всё большие усилия. Кроме того, при столь сложных «очевидениях» было трудно сохранять ясность взгляда на протяжении всего процесса. Такие «очевидения» достигались лишь на мгновение, после чего всё вновь растворялось в тумане неуверенности, и геометр не знал, действительно ли он увидел истину или это было лишь видимостью. Сложность «очевидения» более сложных геометрических истин была обусловлена и тем, что всякий раз, когда геометр хотел использовать, например, теорему Пифагора, он должен был вновь привести её к «очевидению» в данном конкретном случае. По этим причинам некоторые геометры (вероятно, не осознавая этого) отходили от платоновского способа созерцания мира идей и постепенно переходили к шагу, определившему характер всей математики с их времени до наших дней. Этим шагом было введение разума в математику. Если геометр многократно «очевидел» теорему Пифагора, он мог быть полностью уверен в её истинности. Если ему впоследствии требовалось использовать её для «очевидения» другой истины, он понимал, что не обязательно вновь приводить её к «очевидению» в данном случае. Достаточно было знать о её истинности и понимать, что если бы он сейчас её «очевидел», то мог бы «очевидеть» и интересующую его истину. Это рассуждение заменяло последовательность «очевидений». Это была незаметная замена — ведь если бы геометр захотел, он мог бы быть уверен, что на основании этого рассуждения мог бы привести истину к «очевидению». Несмотря на незаметность, это был принципиальный шаг. Геометрические истины больше не требовали непосредственного «очевидения», достаточно было разумного обоснования того, что они могли бы быть «очевидены» при необходимости. Так возникло математическое доказательство.

Вклад Аристотеля в науку своего времени и будущую европейскую науку огромен. Постоянные и неизменные геометрические идеи под его влиянием были заменены лишь представлениями о геометрических объектах. Математика (в то время почти исключительно геометрия), развиваемая под влиянием аристотелевской философии и логики, уже знала логическое доказательство как рассуждение, происходящее на языке^[9], то есть без всяких «очевидений» (поскольку идеи, которые можно «очевидеть», уже не существовали в мире математики). Важной чертой доказательства становится его связь с реальными (то есть воображаемыми) объектами. Эта связь лучше всего выражается в отношении непротиворечивости и осуществимости. Непротиворечивы такие мысленные объекты, из свойств которых нельзя вывести логическое противоречие (то есть нельзя доказать свойство и одновременно его отрицание). Осуществимы же такие объекты, которые можно (хотя бы мысленно) реализовать. Основное логическое правило, установленное Аристотелем, гласит, что ни один объект не может одновременно обладать свойством и его отрицанием. То есть мысленный объект, который противоречив, не может быть осуществим. Обратное утверждение, то есть непротиворечивый объект осуществим, в то время не признавалось^[10]. Например, четыре взаимно перпендикулярных отрезка не противоречат друг другу, но из-за ограничений, накладываемых трёхмерным пространством, их нельзя реализовать или даже представить.

В это время также кристаллизовались основные виды доказательных приёмов, известные как классические схемы логических доказательств^[11]. К ним относятся прямое доказательство, косвенное доказательство, доказательство разбором случаев и доказательство построением (см. раздел Виды математических доказательств).

Аристотелевское понимание математики и математического доказательства отражено в трудах Евклида «Начала», где впервые появляется идея аксиоматического построения математики в виде евклидовых постулатов.

Римская математика в целом никогда не была развитой и по сути оставалась на том уровне знаний, на котором её оставили греки. Прагматичное римское общество признавало только ту часть математики, которая была полезна для строительства и военного дела. Интерес к чистой математике, включая понятие математического доказательства, был практически нулевым.

Математика в целом, особенно в раннем Средневековье, переживала период упадка. Греческое понимание математики и доказательства сохранялось только в Византийской империи. Оттуда с VIII века с этим подходом знакомились Арабы (значительное влияние на арабскую математику оказала и индийская математика). В полной мере арабская математика проявилась в труде Аль-Хорезми Хисаб аль-джабр ва-ль-мукабала (حساب الجبر و المقابلة), где были заложены основы алгебры и связанного с ней нового типа математического доказательства — доказательство вычислением. Этот новый вид доказательства использовался также позднее итальянскими ренессансными математиками при поиске общих решений алгебраических уравнений.

Для понимания математического доказательства в Европе в период с XVI до первой половины XIX века важен термин «область», на которой строилась тогдашняя математика^[12]. Область — это определение некоторого класса осуществимых объектов, для каждого из которых можно (по крайней мере теоретически) решить, принадлежит ли он этой области или нет. Примерами областей могут быть области натуральных чисел, дифференцируемых вещественных функций, а также такие, для которых неизвестно, как они выглядят, или даже пустые, например область всех простых близнецов больше 10^{1 000 000}.

В это время в математике всё ещё был заметен аристотелевский подход — математические объекты не имели постоянного бытия, как платоновские идеи, их можно было только представить или мыслить (осуществить в воображении или мышлении). В осуществлении эти объекты приобретали своё бытие, после ослабления внимания вновь переставали существовать. Область не считалась неким множеством постоянно существующих объектов, а представляла собой выделение тех объектов — существующих, уже исчезнувших, ещё не созданных и даже никогда не существующих, — которые в неё входят (и дуально — не входят). Доказательство «Для любого объекта из данной области верно…» в этом смысле означало доказательство этого утверждения для каждого объекта (даже такого, который никогда не будет осуществлён) этой области. Это понимание совпадает с современным смыслом выражения «для каждого». В отличие от этого, утверждение «Существует объект из данной области, такой что…» не является утверждением. Его истинность не постоянна, поскольку в области, как она здесь определена, объект существует только тогда, когда он осуществлён в мышлении человека. Как только мысль исчезает, такой объект перестаёт существовать, и истинность утверждения может меняться со временем. Чтобы получить утверждение, нужно быть осторожнее и сформулировать его так: «Осуществим объект из данной области, такой что…». Такое утверждение можно доказать только одним способом — осуществив (сконструировав) требуемый объект. Единственным способом доказательства экзистенциальных утверждений в то время было доказательство построением. Чисто экзистенциальное, неконструктивное доказательство по вышеуказанным причинам не использовалось и не могло использоваться. Кроме конструктивного доказательства, за правильное всё ещё считалось доказательство, основанное на геометрическом представлении, без которого тогда при некоторых утверждениях (например, при теореме Больцано) математики не обходились.

Значение чешского философа и математика Бернарда Больцано для развития не только понимания математического доказательства, но и всей математики заключается в замене областей постоянно существующими совокупностями объектов. Из этих совокупностей позднее возникло понятие множества, ставшее центральным в математике XX века. Заметим, что при замене бесконечных областей совокупностями Больцано пришлось столкнуться с проблемой актуальной бесконечности (то есть вопросом, существует ли реально бесконечное множество каких-либо объектов). Эту проблему он смог решить только с помощью теологии, обосновав, что актуально бесконечное множество существует в разуме христианского Бога^[13].

Если заданы постоянно существующие совокупности объектов, то утверждение «Существует объект из данной совокупности, такой что…» уже имеет постоянный характер и является утверждением. Это утверждение можно доказывать двумя способами. Первый — как и в случае областей, сконструировать требуемый объект. Новый способ — доказать лишь существование требуемого объекта без необходимости его строить. Этот новый вид доказательства называется неконструктивным или чисто экзистенциальным. Типичным примером неконструктивного доказательства является доказательство Кантора существования трансцендентных чисел, при котором показывается, что всех алгебраических чисел только счётно много (их можно пронумеровать натуральными числами), а всех вещественных чисел — несчётно много (их нельзя пронумеровать). Поскольку вещественных чисел больше, чем алгебраических, по крайней мере одно трансцендентное число существует. Однако из этого доказательства совершенно не ясно, как найти такое число.

Уже некоторые более ранние философы и теологи (Джордано Бруно, Родриго де Арриага) обосновывали, что объекты, не находящиеся во взаимном логическом противоречии, уже должны быть осуществимы (в разуме Бога)^[14]. Это утверждение, являющееся обратным к классическому аристотелевскому положению о неосуществимости противоречивого, впоследствии утвердилось в математике. Его формализацией на языке современной математической логики является так называемая теорема Гёделя о полноте.

Вследствие работы Больцано в область изучения математики попали такие объекты, существование которых доказуемо, но которые невозможно сконструировать. Примером такого объекта является, например, Непрерывная функция, не имеющая ни в одной точке производной (касательной к графику), открытая независимо сначала Больцано, а затем Вейерштрассом. Грубо говоря, график такой функции можно нарисовать одной линией, но в каждой точке этого графика есть излом, то есть не «гладкая дуга», а «острый угол». Ещё более странным примером может быть Кривая Пеано, то есть инъективная непрерывная кривая, определённая на интервале (0,1), образ которой заполняет весь квадрат (0,1) × (0,1), или функция из вещественных в вещественные числа, принимающая на каждом интервале все вещественные значения. Эти и подобные примеры полностью противоречат человеческой интуиции — Шарль Эрмит о функции Больцано — Вейерштрасса и других подобных примерах говорил: «Я с ужасом отворачиваюсь от этого прискорбного потока непрерывных функций без производной»^[15]. Более существенной для дальнейшего развития математического доказательства была реакция Анри Пуанкаре, который в сочинении La valeur de la Science спрашивал: «Как могла интуиция так нас обмануть?»^[15].

Удивление Пуанкаре понятно, поскольку с появлением вышеуказанных примеров произошло нечто беспрецедентное в математике. Геометрическое представление и интуиция вступили в противоречие с доказуемыми утверждениями. Чтобы избежать противоречивости всей математики, было необходимо отказаться от интуиции и наглядности как доказательных средств. Доказательства многих основных утверждений, особенно математического анализа и геометрии, в то время основывались на наглядности, поэтому их нужно было вновь поставить на твёрдую основу. Такой основой стала аксиоматическая методика, использовавшаяся ещё в античной Греции Евклидом в его «Началах». Однако и Евклид (вероятно, не осознавая этого) в значительной степени опирался на интуицию — об этом свидетельствует, например, тот факт, что у Евклида всего пять постулатов, а Давид Гильберт в своей работе Grundlagen der Geometrie («Основания геометрии») использует для аксиоматизации геометрии 21 постулат. Даже греческий аксиоматический метод оказался недостаточным, и прежде чем на нём можно было построить всю математику, его нужно было полностью очистить от интуиции.

Чаще всего интуиция использовалась в математическом доказательстве. Хотя в геометрии в качестве аксиом выбирались даже самые очевидные истины, чтобы свести использование наглядности к минимуму, сам способ логического вывода следствий из этих аксиом не был аксиоматизирован, и логическое рассуждение применялось свободно. Чтобы полностью исключить интуицию (и, следовательно, всякую неопределённость) из математики, математикам второй половины XIX века пришлось аксиоматизировать само понятие математического доказательства. Одновременно с этим, в стремлении устранить неточности, возникающие из-за (интуитивного) использования естественного языка, происходила формализация этого понятия, то есть замена естественного языка символическим. В работах Давида Гильберта, Готлоба Фреге и других был постепенно разработан формальный символический язык, достаточно богатый, чтобы выразить все математические утверждения, и понятие формального доказательства, позволяющее доказывать формально записанные утверждения (так называемые формулы) с использованием лишь нескольких правил вывода, называемых логическими аксиомами, то есть без малейшего влияния интуиции или наглядности. Математическое доказательство стало чётко определённым понятием, настолько точным, что с появлением современной вычислительной техники его правильность могла быть проверена даже алгоритмически работающим компьютером.

Историческое развитие привело математическое доказательство к такой степени точности, что его правильность может быть проверена компьютером. В настоящее время существуют так называемые системы автоматического доказательства теорем, то есть компьютерные программы, способные строить доказательства математических утверждений. Хотя эти программы иногда способны доказывать и нетривиальные теоремы, они всё ещё далеки от того, чтобы быть практически применимыми. Среди профессиональных математиков нет единого мнения о том, возможно ли создать программу, способную конкурировать с человеком в математическом доказательстве.

Другой способ использования компьютеров в доказательствах — это доказательства под управлением человека, где компьютер используется как помощник в тех частях доказательства, где не требуется изобретательность или абстрактное мышление. Самым известным таким применением компьютера является доказательство теоремы о четырёх красках.

Заметим, что можно доказать математические теоремы, согласно которым не существует ни одной компьютерной программы, способной для любого утверждения определить, доказуемо оно или нет (см. Разрешимость).

Математическое доказательство обычно проводится (формулируется) на естественном языке, в данном случае также называемом метаязыком (например, русский язык в этом смысле — метаязык). Использование естественного языка, который часто многозначен, приводит (особенно при неопытности пользователя) к неточностям и ошибкам. Использование естественного языка также приводит к множеству парадоксов (см. Парадокс Рассела, Парадокс лжеца или Парадокс ста слов). Доказательство, проводимое на естественном языке, называется неформальным доказательством. Стремление устранить неточности, связанные с использованием естественного языка, привело в конце XIX и начале XX века к возникновению математической логики и созданию понятия формального доказательства, в котором использование естественного языка полностью устранено (заменено формальным языком). Из-за трудоёмкости (особенно временной) составления формальных доказательств даже в современной математике однозначно доминирует неформальное доказательство, недостатки которого обычно не приводят к ошибкам у опытного пользователя (математика).

Неформальное доказательство — это доказательство на естественном языке, основанное на заданных предпосылках и правилах разума. По историческим причинам различают несколько основных видов (неформальных) доказательств.

Прямое доказательство — это способ, при котором доказываемое утверждение выводится прямым применением определений, предпосылок и ранее доказанных утверждений, иначе говоря, выводится методом «если… то…» или «…следовательно…».

Косвенное доказательство — это метод, используемый для доказательства утверждений типа «если A, то B», при котором доказывается «если не B, то не A». Оно тесно связано с доказательством от противного — любое косвенное доказательство может быть легко сведено к доказательству от противного.

Доказательство от противного основано на использовании ложной предпосылки, которая затем приводит к противоречию (из неё выводится явно ложное утверждение). Если это происходит, доказывается ложность данной предпосылки, а значит, истинность её противоположности. Доказательство от противного близко к косвенному доказательству — любое косвенное доказательство может быть легко сведено к доказательству от противного.

Доказательство индукцией заключается в доказательстве утверждения типа «для всех объектов некоторого класса верно…» способом, при котором объекты данного класса делятся на несколько (чаще всего бесконечно много) подклассов, которые упорядочиваются в последовательность и о них доказывается:

1. (база индукции) Для всех объектов из первого подкласса верно…
2. (индукционный шаг) Если верно … для всех объектов из предыдущих подклассов, то верно… и для всех объектов из следующего подкласса.

Существует много видов доказательств индукцией:

• Математическая индукция (все подклассы однопредметные, а последовательность счётна)
• Трансфинитная индукция (все подклассы однопредметные, а последовательность может иметь любую кардинальность)
• Фундированная индукция
• Индукция по сложности

Доказательство построением — это метод доказательства экзистенциальных утверждений «существует X такой, что…», при котором строится (конструируется) объект X, для которого … выполняется. Этот вид доказательства иногда называют доказательством приведением примера.

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

Неконструктивное доказательство экзистенциального утверждения «существует X такой, что…» — это такое доказательство, которое доказывает существование такого X, но не позволяет получить ни одного примера объекта, который мог бы быть выбран в качестве X. Этот вид доказательства сегодня в основном признаётся правильным, но в прошлом (особенно на рубеже XIX и XX века) многие выдающиеся математики протестовали против такого способа доказательства и не признавали утверждения, доказанные этим способом. В современной математике существует самостоятельное направление — конструктивизм, стремящийся доказывать все утверждения конструктивно (см. Интуиционистская логика). Пионерами в области неконструктивных доказательств были Георг Кантор (доказательство существования трансцендентных чисел) и особенно Давид Гильберт. Проблематика неконструктивных доказательств тесно связана с аксиомой выбора и существованием (непротиворечивостью) актуальной бесконечности.

Геометрическое доказательство — это доказательство, использующее методы геометрии. Его наглядность во многом определяется возможностью геометрического представления, однако строгое геометрическое доказательство не должно основываться только на наглядности. Геометрические доказательства чаще всего используются в самой геометрии, но также часто встречаются в математическом анализе и теории чисел.

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

Формальное доказательство — это доказательство, проводимое не на естественном языке, а на символическом — формальном. Для минимизации неточностей, которые часто встречаются в неформальных доказательствах, все утверждения в формальном доказательстве рассматриваются как конечные последовательности символов (так называемые формулы, иногда секвенции), и вводится система правил, определяющих, как с этими последовательностями обращаться. Эта система правил называется логическим исчислением. Два наиболее распространённых исчисления — гильбертовское и гентценовское. Каждое из этих исчислений состоит из логических аксиом, выражающих основные свойства логических связок и кванторов, и правил вывода, определяющих, как из предпосылок выводить их следствия.

Формальное доказательство в гильбертовском исчислении определяется как конечная последовательность формул, одна из которых, обычно последняя, выражает доказываемое утверждение, и каждый член которой является либо

• логической аксиомой,
• собственной аксиомой теории, в которой ведётся доказательство,
• выведен из предыдущих членов по одному из правил вывода (см. Гильбертовское исчисление).

Гентценовское исчисление отличается от гильбертовского тем, что доказываются не формулы, а так называемые секвенции, то есть символы вида ${\displaystyle <A\Rightarrow B>}$, где ${\displaystyle A}$, ${\displaystyle B}$ — конечные множества формул. Символ ${\displaystyle <A\Rightarrow B>}$ означает: «Если все формулы из A верны, то верна хотя бы одна формула из B». Доказательством формулы ${\displaystyle \varphi }$ считается доказательство секвенции ${\displaystyle <\emptyset \Rightarrow \{\varphi \}>}$.

До XX века предполагалось, что любое доказательство может быть в принципе проверено компетентным математиком для подтверждения его правильности^[16]. В настоящее время компьютеры используются как для доказательства теорем, так и для выполнения вычислений, слишком длинных для проверки человеком или группой людей; примером компьютерного доказательства является и самое раннее доказательство теоремы о четырёх красках 1976 года. Некоторые математики опасаются, что возможность ошибки в компьютерной программе или сбоя при её выполнении ставит под сомнение правильность таких компьютерных доказательств. На практике вероятность того, что ошибка сделает компьютерное доказательство недействительным, можно снизить за счёт включения избыточности и самопроверки в вычисления, а также создания нескольких независимых подходов и программ. Ошибки нельзя полностью исключить и при проверке доказательства человеком, особенно если доказательство содержит естественный язык и требует глубокого математического понимания для выявления скрытых предпосылок и ошибок.

Великая теорема Ферма формулируется так:

Не существует положительных целых чисел x, y и z таких, что xⁿ + yⁿ = zⁿ для некоторого натурального числа n, большего 2.

Это — одна из самых известных теорем во всей истории математики. История её доказательства тянется от средневековых арабских математиков до самого конца XX века, попытки её доказательства регулярно и существенно влияли на развитие всей математической науки, особенно алгебры и алгебраической теории чисел^[17].

Вероятно, уже средневековые арабские математики знали о справедливости великой теоремы Ферма для случая n = 3, однако их доказательства не сохранились^[18]. Самое раннее сохранившееся доказательство для этого случая принадлежит Леонарду Эйлеру.

Сам Пьер Ферма доказал случай n = 4, построив для любого возможного решения этого уравнения меньшее решение. Так он получил бесконечно убывающую последовательность натуральных чисел, то есть противоречие.

В 1825 году Петер Дирихле и Адриен-Мари Лежандр доказали случай n = 5, а в 1839 году Габриэль Ламе — n = 7.

В 1847 году Эрнст Куммер доказал теорему Ферма для всех регулярных простых чисел, к которым относятся все простые числа меньше 100, кроме 2, 37, 59 и 67.

Общий случай великой теоремы Ферма был доказан в 1995 году Эндрю Уайлсом после того, как в его первоначальном доказательстве 1993 года была обнаружена ошибка. Доказательство великой теоремы Ферма уникально во многих отношениях. Его объём превышает 100 страниц печатного текста, оно было создано в результате девятилетней работы одного математика, а главное — объединяет множество различных, иногда весьма отдалённых областей математики: теорию диофантовых уравнений, модулярные формы, алгебраическую геометрию, теорию Галуа и другие. Благодаря этому оно считается важным шагом к реализации так называемой программы Ленглендса по объединению теории чисел и теории представлений. Это также яркий пример того, насколько сложным может быть доказательство просто сформулированного утверждения.

Теорема о четырёх красках утверждает, что любую карту на плоскости можно раскрасить четырьмя красками так, чтобы любые два соседних региона имели разные цвета. Гипотеза о справедливости этого утверждения была выдвинута ещё в 1852 году молодым математиком Фрэнсисом Гатри. В 1878 году эта гипотеза стала широко известна, когда Артур Кэли обратился ко всем участникам заседания Лондонского математического общества с просьбой попытаться её доказать. Однако гипотеза оставалась недоказанной почти сто лет. Только в 1976 году Кеннет Аппель и Вольфганг Хакен объявили, что нашли доказательство.

Аппелю и Хакену удалось свести всю проблему четырёх красок к конечному числу случаев, которые нужно было рассмотреть. Однако этих случаев было так много (1936), что их ручная проверка заняла бы у одного человека всю жизнь, и всё равно он не успел бы их все проверить. Поэтому проверка этих случаев была поручена компьютеру, который затратил на это более 1200 часов машинного времени. Такое использование компьютера для доказательства математической теоремы вызвало в своё время бурную полемику. Ни один человек уже не мог проверить правильность доказательства — можно было вручную проверить правильность программы, которая проверяла отдельные случаи, но это не исключало возможности аппаратной ошибки, которая могла бы сделать всё доказательство недействительным. В защиту компьютерных доказательств приводился аргумент, что при столь сложных и длинных доказательствах вероятность аппаратной ошибки хоть и не нулевая, но гораздо меньше вероятности аналогичной ошибки человека^[19]. В настоящее время теорема о четырёх красках считается доказанной, и против использования компьютеров в математических доказательствах серьёзных возражений не выдвигается.

Следует добавить, что Аппель и Хакен считали своё доказательство лишь первым из ряда, в которых компьютеры будут играть существенную роль^[19]. Однако таких доказательств немного; можно привести, например, доказательство несуществования проективной плоскости порядка 10, доказательство гипотезы Роббинса и несколько доказательств, касающихся выигрышных стратегий в некоторых конечных играх.

Теорема о классификации конечных простых групп утверждает, что любая конечная простая группа либо принадлежит одной из 18 бесконечных серий групп, либо является одной из 26 так называемых спорадических групп. Таким образом, эта теорема полностью описывает все конечные простые группы. Из-за огромной сложности её доказательства в английском языке она также называется «Enormous theorem».

Доказательство этой теоремы никогда не публиковалось целиком. Оно состоит из более чем 500 статей примерно 100 авторов, опубликованных в различных математических журналах преимущественно между 1955 и 1983 годами. Оценивается, что общая длина доказательства составляет 10 000–15 000 страниц печатного текста^[20]. Такая масштабность может вызвать (как и в случае теоремы о четырёх красках) сомнения в правильности доказательства. Вероятно, ни один математик не прочитал это доказательство целиком, и, следовательно, никто в мире не может утверждать, что в нём нет ошибки. Однако каждая отдельная часть доказательства, опубликованная за почти тридцать лет, была прочитана и признана правильной многими математиками. Поэтому это доказательство считается правильным, хотя ни один конкретный человек никогда не проверял его полностью и, вероятно, не проверит в будущем.

Учитывая невероятную длину доказательства, весьма вероятно, что оно содержит множество мелких ошибок и неточностей. Один из главных авторов доказательства Майкл Ашбахер сказал по этому поводу: «Вероятность ошибки в классификационной теореме практически равна 1. С другой стороны, вероятность того, что каждая из этих ошибок не будет легко исправлена, практически равна нулю, и поскольку доказательство конечно, вероятность того, что теорема неверна, очень близка к нулю. По мере того как проходит время и мы лучше знакомимся с доказательством, наша уверенность в нём только растёт.»^[20]

Иногда для обозначения конца доказательства пишут сокращение Q.E.D.. Эта аббревиатура означает «quod erat demonstrandum», что по-латыни значит «что и требовалось доказать». В русском языке иногда используется сокращение ч. т. д. В современной математике чаще для окончания доказательства используют символ ${\displaystyle \blacksquare }$ или ${\displaystyle \square }$, называемый просто «квадратик» или символ Халмоша в честь Пола Халмоша, который ввёл его в употребление. При написании "Q.E.D." или ч. т. д., а также при устной презентации произносится: «что и требовалось доказать». В Unicode специально предусмотрен символ «конец доказательства», U+220E (${\displaystyle \blacksquare }$) (220E(hex) = 8718(dec)).