Эпистемологические нормы и социальные практики математического доказательства

Размещено на http://www.allbest.ru/

Эпистемологические нормы и социальные практики математического доказательства

А.В. Хлебалин

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

Ключевые слова: социальная и эпистемологическая экспертиза, компьютерная математика, математическая практика.

Aleksandr V. Khlebalin,

EPISTEMOLOGICAL NORMS AND SOCIAL PRACTICES OF MATHEMATICAL PROOF

Keywords: social and epistemological examination; computer mathematics; mathematical practice. эпистемологический компьютерная математика

The study is supported by the Russian Foundation for Basic Research, Project No. 19-01100301.

The widespread use of computers not only in obtaining or verifying mathematical results, but also as a means of organizing the mathematical community, will allow solving the problem of examining mathematical results and will also significantly change the epistemic characteristics of mathematical knowledge as knowledge generated and verified individually. The emerging mathematical Internet platforms pretend to act as independent structural elements of the “map of mathematical knowledge”. They can often act as collective agents of mathematical activity. The creation of libraries of computational mathematics is the creation of unparalleled database structures that organize collective mathematical knowledge in an optimal way (historians of science emphasize the extraordinary importance of the invention of a library catalog for the development of science; it is difficult to imagine the scale of the stimulus for the development of computational mathematics as a result of the creation of such a new organization of mathematical knowledge). The most controversial aspect of computer knowledge, associated with the verification of boundless computer proofs, is also going through an essential stage associated with the development of the theory of univalent foundations. This theory claims to act not only as new foundations of mathematics, but also, due to its formalizability, as the basis of computer mathematics. The transformation of mathematical practice, caused by the introduction of computers both in the organization of the mathematical community and directly in the mathematical practice of obtaining and verifying results, indicates that the very social practice of examining and consolidating mathematical results is undergoing revolutionary changes in its scale. In the sociology of science and technology, a new direction of research is being formed - the social machine - associated with the study of the transformation of social practices on the basis of the emergence of human-computer cooperation in them. In the author's opinion, the development of computer mathematics turns the practice of modern mathematics into a most interesting field of research in this direction due to both the speed of the changes taking place and their scale. The first studies of this kind convincingly demonstrate the depth of the transformation of the accepted social standards of examination and the consolidation of mathematical results in connection with the increasing introduction of the computer into mathematical practice. In the author's opinion, the most intensive changes in the mathematical practice of production and verification of knowledge will be associated with the further development of the program of univalent foundations, which claims to be the foundations of both computational and most of mathematics in general.

Обсуждение эпистемологических характеристик результатов, полученных с помощью компьютера, - прежде всего, вопросов, связанных с его приемлемостью, обоснованностью, обозримостью и аргументативной силой, - инициируется, как правило, оппонентами вычислительной, или компьютерной, математики. Обсуждение эпистемологического статуса результатов, полученных с помощью компьютера, вызвано их явными несоответствиями классической модели математического знания. Обозначим ее как «наивную» на манер принятого обозначения канторовской теории множеств, специально отметив, что это обозначение не содержит никаких оценочных, а тем более уничижительных характеристик. Эта модель, а точнее обобщенная картина математического знания, является неким социально-историческим конструктом, представляющим собой соединение элементов различных концепций, отчасти заимствованных из эпохи поиска оснований математики, отчасти из кульминационных этапов развития математики в прошлом. Такая картина характеризует математику как исключительно дедуктивную, построенную на основе вывода теорем с помощью надежных правил из непроблематичных аксиом, которые принято в этой картине характеризовать как «очевидные, не нуждающиеся в обосновании» положения. Истоки такой картины восходят к провозглашению «Начал» Евклида образцом математики. В этом смысле «наивная» концепция выполняла скорее декларативную, нормативную роль, чем описывала реальное развитие математики; здесь достаточно вспомнить классическую работу М. Клайна [1], представляющую развитие математики как все большее отдаление от провозглашенного образца, верность которому тщательно сохранялась, но практическая реализация которого постоянно откладывалась. Поэтому более правильным будет считать эту «наивную» концепцию скорее идеологией, чем теорией, направленной на описание и объяснение реальной математической практики в тот или иной момент истории математики. В истории и философии науки широкое хождение имеет термин «виговская история науки», выражающий идеал науки как обреченного на прогресс, постоянного накопления знания. Аналогией этой идеологии может быть «наивная» концепция математики. Как и в случае с «виговской» концепцией развития науки, в случае с «наивной» концепцией математики невозможно вести речь о подлинном авторстве концепции; ее элемент можно обнаружить у большого количества авторов, даже среди тех, чьи воззрения были откровенно враждебны друг другу. Такая своего рода «дисперсия» и производит впечатление «естественности» или «наивности» идеологическойконцепции.

Применение компьютеров в верификации, а затем и в генерировании нового математического знания, очевидно, не укладывается в «наивную» идеологию. Сама характеристика таких результатов, как «экспериментальная математика» или «вычислительная математика», выражает те аспекты традиционной идеологии, которые нарушаются при использовании компьютера в математической практике. Например, существенная роль, которую играет конкретная машина и единичный или повторенный конечное количество раз случай реализации ею конкретной программы, привносит эмпирический элемент в математическое исследование, который вовсе не соответствует исключительно дедуктивному пониманию математики. Гигантские объемы математических результатов не позволяют рассчитывать на то, чтобы человек мог бы понять и проверить правильность полученного машиной результата. Компьютерная математика оказалась вызовом «наивной» идеологии математики. Идеологический накал обсуждения компьютерных результатов каждой из сторон - как сторонников, так и противников признания этих результатов как подлинно математических - очевиден. Например, явно угадывается идеологический элемент в провозглашении Дж. Хорганом «смерти доказательства» [2], так же как он угадывается и в предвидении В. Воеводским того, что через десть лет серьезный математический журнал не примет к публикации работу, к которой не будет приложен прувер. Этот идеологический накал дискуссии, на наш взгляд, не должен рассматриваться как обесценивающий ее. Напротив, для нас он указывает на происходящие существенные изменения в социальной практике принятия математических результатов. Изменения эти касаются трансформации как «карты математического знания», так и способов ее формирования и трансформации.

Возражения странника «наивной» идеологии против компьютерных математических результатов хорошо известны со времен осуждения доказательства теоремы о четырех красках, инициированного в философии математики Т. Тимошко [3]. Не углубляясь в саму эту дискуссию, просто отметим основные. Прежде всего, это необозримость компьютерных доказательств, их эмпирическая составляющая, которой мы обязаны машине и реализации ею программы, неприменимость к ним каких-либо когнитивных характеристик вроде «понимание». Действительно, статус таких доказательств проблематичен для «наивной» концепции математики. Как можно, например, всерьез говорить о понимании доказательства «булевых пифагоровых троек», если оно содержит в себе 200 терабайт данных? Ни о каком понимании или обозримости речь здесь не может идти в принципе. Проверка правильности работы программы, которая одновременно является и технической, и теоретической проблемой, осложняет процедуру верификации и принятия результаты работы компьютера как верного. Но даже если допустить существование абсолютно надежного, не вызывающего никаких сомнений средства верификации функционирования машины и верности совершенных вычислений, встает вопрос о том, готово ли математическое сообщество принять результат в качестве собственно математического?

Гигантские объемы компьютерного доказательства, вызывающие столь сильные претензии к их принятию, тем не менее, не являются следствием того, что компьютеры достигли таких мощностей, которые сделали возможным их применение в решении сложных математических задач. Сложность вычислительных результатов, на наш взгляд, является одним из аспектов усложнения математических задач в целом. «Человеческой» математике хорошо известны столь же сложные результаты, полученные без участия компьютера. Например, известная теорема о классификации простых конечных групп. Результат, полученный около ста учеными, публиковавшийся на протяжении практически пятидесяти лет и насчитывающий в общей сложности тысячу страниц, конечно, посвоим «размерам» уступает полученному компьютером результату о булевых пифагоровых тройках, но не исчезает ли это различие в случае попытки обозреть и понять доказательство о конечных граппах одним человеком? Иной пример, ставший также широко известным, - это случай с попытками доказательства Луи де Бранжем гипотезы Римана. Привлекший к этому случаю внимание не только математиков, но и посторонней публики К. Саббаг [4] не скрывает своего удивления тем, что коллеги пренебрегают проверкой превенции на решение знаменитой задачи. Среди факторов, приведших к столь неоднозначной ситуации, фигурируют сплошь социальные, связанные с нескрываемой конкуренцией за первенство в получении результата, апелляцией к неоднозначной репутации и пр. Но особенно интересной представляется ссылка на сложность доказательства: «Де Бранж сейчас заявляет, что решил другую проблему, гораздо более значимую, чем проблема Бибербаха, и опять-таки решение найдено с помощью „совсем неожиданных источников“, и опять люди считают это заявление фантастикой. Так не придет ли математическое сообщество в очередной раз к признанию полученного им результата? Вряд ли, ибо никто так и не удосужился прочитать статью, насчитывающую 121 страницу, для того чтобы составить о доказательстве компетентное мнение. Поскольку де Бранж в своем доказательстве использует математические средства, экспертом в которых является он сам и немногочисленная группа математиков, прежде чем приступить к оценке самого доказательства, необходимо изучить огромный материал. А это требует слишком многого времени. Даже немногие математики из тех, кто знает де Бранжа и понимает его метод, страшатся этого трудоемкого дела» [4.C. 113].Предшествующий результат Л. де Бранжа, принесший ему славу, связанный с доказательством теоремы Бибербаха, было, по выражению П. Сарнака, «абсолютно блестящим, по-настоящему великолепным» [4.C. 113], для верификации которого потребовалось несколько месяцев работы целой группы математиков Института математики им. Стеклова.

Л. де Бранж претендует на решение одной из самых известных «задач тысячелетия», которая также занимает весьма интересное положение на «карте математического знания». Помимо невероятно богатой истории попыток ее доказать, гипотеза Римана лежит в основании большого числа математически результатов. Мнения математиков в отношении истинности гипотезы Римана полярны: наряду с большим числом математиков, верящих в ее истинность, есть и сторонники мнения А. Тьюринга, полагающие ее ложной. Аналогично существуют разные мнения о том, будет ли достигнуто когда- либо - а если будет, то какими средствами, - доказательство истинности или ложности гипотезы Римана. Э. Одлыжко, один из авторов закона Монтгоме-ри-Одлыжко, так иронически характеризует вопрос о статусе гипотезы Римана: «Сказано, что, кто бы ни доказал истинность теоремы о распределении больших чисел, тот достигнет бессмертия. И верно: и Адамар, и де ля Валле Пуссен дожили до девяноста с лишним лет. Возможно, гипотеза Римана; но если кто-нибудь сумеет доказать ее ложность - найти нуль вне критической прямой, - то он умрет на месте и о его результате никто никогда не узнает» [5.C. 422]. Но статус недоказанной, пусть и существенно верифицированной вычислительными средствами, гипотезы не мешает большому числу математиков основывать на ней свои исследования. И по этому поводу Э. Олдышко высказывает опасения: «Как рецензент и редактор журналов я часто имею дело со статьями, начинающимися со следующих слов: „исходя из истинности гипотезы Римана“... Такие выражения никого не смущают; но страшно подумать, что нам делать со всем этим, со всеми присвоенными степенями и полученными грантами, если окажется, что гипотеза Римана ложна» [5.C. 431].

Эти иллюстрации можно продолжить; они явно демонстрируют, что уровень сложности современных проблем математики таков, что применительно ко многим из них вопрос об их верификации является проблематичным с позиции «наивной» концепции. Сложно ожидать в случае тех результатов, которые признаются сообществом «выдающимися» и «интересными», того, что типичный математик может их обозреть и понять. Признание таких результатов вроде доказательства теоремы Бибербаха основано на компетентном мнении немногих признанных экспертов, порой целых коллективов экспертов. Институт математической экспертизы является очень сложным социальным институтом, и то, в какой степени он воплощает эпистемологические добродетели, предусмотренные «наивной» математической идеологией, является самостоятельным нетривиальным вопросом. То, что эта идеология не соответствует всему тому многообразию доказательства, которое характеризует математическую практику, даже если исключить из нее компьютерные математические результаты, очевидно и философам математики, и профессиональным математикам. Социологический фактор преодолевает несоответствие многообразия практики доказательства заявляемым «наивной» концепцией стандартам. Здесь нужно отметить исторический характер представлений о строгости доказательства, которые всякий раз кодифицируются определенной социальной практикой экспертизы и принятия результата, превышающей своим разнообразием декларируемые нормативные стандарты.

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

«Наивная» концепция математики имплицитно предполагает математическую деятельность в качестве индивидуальной. Она по преимуществу и была такой на протяжении тысячелетия. Сами математики оставили огромное количество свидетельств о математическом творчестве как сугубо индивидуальном, зачастую предполагающем подлинный «уход от мира»: «Каждое утро я сажусь перед чистым листом бумаги. В течение дня, с коротким обеденным перерывом, я все смотрю и смотрю на чистый лист. Порой, когда наступает вечер, он все еще пуст. Два лета - 1903 и 1904 годов - останутся в моей памяти как период полного интеллектуального тупика... Вполне вероятно, что весь остаток моей жизни может пройти за разглядыванием этого чистого листа» (цит. по: [5.С. 427]). Это свидетельство из «Автобиографии» Рассела вполне типично; более плодотворные минуты творчества характеризуются также в индивидуальном стиле. Например, Э. Уайлс чуть ли не в мистических терминах описывает доказательство теоремы Ферма: «...иногда я понимал, что ничего из того, что было сделано раньше, не пригодится. Тогда я принимался за что-то совершенно новое; мистика, откуда это все приходило» [6].

Однако эта индивидуалистическая парадигма математического творчества была поставлена под сомнение еще в XVIII в.; напомним часто цитируемый пассаж из Д. Юма: «Нет такого алгебраиста или математика, который был бы настолько сведущ в своей науке, чтобы вполне доверять любой истине тотчас же после ее открытия или же смотреть на нее иначе, чем на простую вероятность. С каждым новым обозрением доказательств его доверие увеличивается, но еще более увеличивается оно при одобрении его друзей и достигает высшей степени в случае общего признания и одобрения всем ученым миром» [7.C. 266]. Приведенные выше примеры показывают, что рост сложности математических результатов, необозримость доказательства, коллективно оплаченные результаты вроде классификации конечных простых групп превращают социальную экспертизу в насущную проблему развития математики. Полученные с помощью компьютера результаты обычно рассматриваются как не подлежащие традиционным способам экспертизы, как воплощающие в себе все те характеристики, которые попросту делают ее невозможной. В наиболее острой форме проблема экспертизы полученных компьютером результатов приводит к противопоставлению «человеческой» и «компьютерной» математики, как, например, в широко известном заявлении, сделанном в 1979 г. де Милло, Липтоном и Перлисом, в котором утверждалось [8], что «математические доказательства увеличивают нашу уверенность в истинности математических утверждений только после того, как они были подвергнуты оценке социальными механизмами математического сообщества», а по поводу роста компьютерных доказательств, не подлежащих ей, авторы выражают озабоченность «символическим шовинизмом», передающим право экспертизы компьютерным программам.

Нам представляется, что широкое распространение компьютерных средств не только в получении или проверке математических результатов, но и как средства организации математического сообщества не только позволит решать проблему экспертизы математических результатов, но и существенно изменит эпистемические характеристики социальной экспертизы. По-видимому, математическое сообщество первым и в наибольшей степени было трансформировано компьютерными средствами коммуникации. Речь идет не о банальном упрощении коммуникации между учеными. Появление таких интернет-платформ, как mathoverflow, arXiv(упомянем только наиболее известные, полный перечень таких интернет-сообществ невероятно большой и постоянно расширяется), претендует на самостоятельные структурные элементы «карты математического знания». Их особенностью является то, что они предоставляют возможность перманентной экспертизы на любом этапе математической деятельности. Зачастую они могут выступать как коллективные агенты математической деятельности. Далее, образование (и вновь нужно отметить постоянный рост числа) библиотек вычислительной математики, содержащих обширные коллекции математических результатов, полученных средствами отдельных языков программирования, представляет собой создание не имеющих аналогов структур баз данных, организующих коллективное математическое знание оптимальным способом (историки науки подчеркивают необычайное значение дляразвитие науки изобретения библиотечного каталога; сложно предположить, какого масштаба будет стимул развития вычислительной математики в результате создания такой новой организации математического знания). Наконец, наиболее дискуссионный аспект компьютерного знания, связанный с верификацией необозримых компьютерных доказательств, также переживает существенно важный этап, связанный с разработкой теории унивалентных оснований, претендующей выступить не только в роли новых оснований математики [9], но и, в силу формализуемости, основанием компьютерной математики [10].

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

Литература

1. КлайнМ. Математика. Утрата определенности. М. : Мир, 1984. 446 с.

2. Horgan J. The death of proof // Scientific American. 1993. October. P. 93-103.

3. Tymoczko T. Computers, Proofs and Mathematicians: A Philosophical Investigation of the Four-Color Proof // Mathematics Magazine. May 1980. Vol. 53, № 3. P. 136-137.

4. Саббаг К. Странный случай Луи де Бранжа // Целищев В.В. Аномалии знания: идеи и люди. М. : Канон+ РООИ «Реабелитация», 2020. С. 83-107.

5. Дербишер Дж. Простая одержимость: Бернхард Риман и величайшая нерешенная проблема в математике. М. :Астрель : Corpus, 2010. 463с.

6. Wiles A.J. Interview on PBS (2000). URL: http://www.pbs.org/wgbh/nova/physics/andrew- wiles-fermat.html

7. ЮмД. Трактат о человеческой природе. М. : Канон, 1995. Кн. I. 379 с.

8. DeMillo R.A., Lipton R.J., Perlis A.J. Social processes and proofs of theorems and programs // Commun. 1979. ACM 22 (5). Р. 271-280.

9. PelayoA.,WarrenM.Homotopy type theory and Voevodsky's univalent foundations // Bulletin of the American Mathematical Society. 2014. Vol. 51, № 4. Р. 597-648.

10. Voevodsky V. An experimental library of formalized Mathematics based on the univalent foundations // Mathematical Structures in Computer Science. 2015. Vol. 25, is. 5. P. 1278-1294.

References

1. Kline, M. (1984) Matematika. Utrataopredelennosti [Mathematics. The Loss of Certainty]. Translated from English. Moscow: Mir.

2. Horgan, J. (1993) The death of proof. Scientific American. October. pp. 93-103.

3. Tymoczko, T. (1980) Computers, Proofs and Mathematicians: A Philosophical Investigation of the Four-Color Proof. Mathematics Magazine. 53(3). pp. 136-137. DOI:

10.1080/0025570X. 1980.11976844

4. Sabbag, K. (2020) StrannyysluchayLui de Branzha [The strange case of Louis de Branges]. In: Tselishchev, V.V. Anomaliiznaniya: ideiilyudi [Knowledge Anomalies: Ideas and People]. Moscow: Kanon+ ROOI “Reabelitatsiya”. pp. 83-107.

5. Derbyshire, J. (2010) Prostayaoderzhimost': BernkhardRimanivelichayshayanereshennayaproblema v matematike [Prime Obsession: Bernhard Riemann and the Greatest Unsolved Problem in Mathematics]. Translated from English. Moscow: Astrel': Corpus.

6. Wiles, A.J. (2000) Interview on PBS. [Online] Available from: http://www.pbs.org/wgbh/no- va/physics/andrew-wiles-fermat.html

7. Hume, D. (1995) Traktat o chelovecheskoyprirode [Treatise on Human Nature]. Vol. 1. Translated from English. Moscow: Kanon.

8. DeMillo, R.A., Lipton, R.J. & Perlis, A.J. (1979) Social processes and proofs of theorems and programs. Commun.ACM 22(5). pp. 271-280.

8. Pelayo, A. & Warren, M. (2014) Homotopy type theory and Voevodsky's univalent foundations. Bulletin of the American Mathematical Society.51(4). pp. 597-648.

10. Voevodsky, V. (2015) An experimental library of formalized Mathematics based on the univalent foundations. Mathematical Structures in Computer Science.25(5). pp. 1278-1294. DOI: 10.1017/S0960129514000486

Размещено на Allbest.ru