Знание-сила, 2008 № 06 (972)

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

Даже в моей небогатой научной практике было уже два случая, когда в доказательстве математических фактов помогал компьютер. В одном случае мы написали программу, которая проводила вычисления в достаточно хитром кольце (через сведение к кольцу многочленов, конечно, но сведение тоже проводил компьютер). По результатам этих вычислений мы пришли к неким математическим выводам. Другой случай был даже более рафинированным: компьютер перебирал все возможные случаи, и на основе этого полного перебора, опираясь на то, что действительно все варианты были исследованы, мы доказали требуемую нижнюю оценку.

Можно ли считать, что в этих случаях мы получили доказательство? Бог с ними, с другими людьми, я сам, автор, могу быть уверен, что доказал что-то? А если я ошибся, когда писал программу? Программисты знают: вопрос не в том, есть ли в программе баги, а в том, когда они обнаружатся. А специалисты по верификации знают, что доказать корректность компьютерной программы зачастую гораздо сложнее, чем убедиться в корректности математического доказательства. Здесь не надо путать корректность алгоритма (как математического объекта) с корректностью самого кода программы: если проверить алгоритм обычно можно теми же методами, что и обычное доказательство, то анализ кода — очень сложная задача. И чтобы быть уверенным, что моя программа работает правильно, проверять надо именно код, а не идею алгоритма (она-то, конечно, и проверена, и в статьях изложена).

Под влиянием всех этих факторов у некоторых исследователей создается впечатление, что с развитием математики (в частности, с появлением все более и более сложных и длинных доказательств) доказательства теряют свое главное свойство — убедительность. Что же тогда остается от доказательства: ведь убедительность, казалось бы, — единственное, что от него требуется? Кроме того, с усложнением доказательства возрастает его элемент субъективности: математик уже не просто по собственной лености верит и не проверяет — он физически не способен этого сделать. Получается, что хотя все доказательства должны, по определению, быть убедительными, на деле одни из них (более простые) убедительнее других (более сложных). То есть простые доказательства как бы «в большей степени являются доказательствами», чем сложные! Из-за этого некоторые авторы начинают говорить чуть ли не о «болезни» современной математики (о кантовской болезни, продиагностированной Пуанкаре, они уже не вспоминают — видимо, перешла в хроническую фазу и лечению не подлежит).

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

И можно в итоге сделать неутешительный вывод: с чего начали, к тому и возвращаемся. Записано на папирусе авторитетным человеком — значит, верно. Проверять доказательства люди по большому счету разучились и, раз джинн выпущен из бутылки, уже не научатся. Выше я писал о классификации конечных простых групп; прелесть ситуации в том, что на эту теорему, метко прозванную «the enormous theorem», с 1983 года, когда она была полностью опубликована, до 2003 года ссылались с опаской. Прошло двадцать лет, а это доказательство (записанное даже без ссылок на компьютерные вычисления!), ключевое для целых немаленьких областей науки, по большому счету оставалось непроверенным, и находились математики, которые в него не верили. Причем не какие-нибудь маргиналы — в классификацию не верил, например, один из величайших алгебраистов современности Жан-Пьер Серр. Лишь в 2003 году вышла статья Ашбахера, окончательно расставившая все точки над i. О какой же математической истине можно вообще говорить в наше время?

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

Грибки и плесень могут не только быть опасными и вредными, но и приносить людям немалую пользу. Например, португальские ученые с их помощью надеются избавить человечество от мусора и отходов. Сотрудники Технологического института химии и биологии выделили около 500 видов грибков, способных перерабатывать самые трудноразлагаемые вещества.

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

Обезвоживание осадков, образующихся на станциях очистки сточных вод, представляет собой сложную проблему, до сих пор не решенную с достаточной эффективностью. При этом надо заметить, что осадок состоит на 90 — 95% из воды. Если воду убрать, то тонна осадка превратится в 50 — 100 килограммов сухого вещества, занимающего не так уж и много места. К тому же избавление от одной тонны осадка, например в Германии, стоит 75 — 100 евро (а страна «производит» примерно 60 миллионов тонн осадка сточных вод ежегодно).