Команда математиков за полгода написала 600-страничную книгу, используя GitHub

Перевод статьи Андрея Бауера — The HoTT book ^[1]

Книга по HoTT закончена!

Начиная с весны, и даже раньше, я участвовал в командном проекте по написанию книги по гомотопической теории типов (Homotopy Type Theory ^[2]). Она наконец написана и готова к употреблению. Вы можете скачать книгу бесплатно: homotopytypetheory.org/book/ ^[3]. Майк Шульман рассказал о содержании книги ^[4], так что я не буду повторять то же самое. Вместо этого я бы хотел прокомментировать некоторые социо-технологические аспекты создания книги и, в частности, рассказать о том, чему нас научило сообщество Open source.

Мы — две дюжины математиков, написавших 600-страничную книгу меньше чем за полгода. Это впечатляет, поскольку обычно математики не работают большими группами. В маленькой группе математики могут позволить себе использовать устаревшие технологии — например, пересылать друг другу исходники LaTeX по электронной почте, — но когда математиков больше двадцати, их не спасает даже Dropbox. К счастью, многие из нас — специалисты по Computer Science, замаскированные под математиков, так что мы знали, как справиться с логистикой. Мы использовали git ^[5] и github.com ^[6]. Потребовалось время, чтобы привыкнуть, но никаких реальных сложностей не возникло. В конце репозиторий стал не только архивом для наших файлов, но также центральным хабом для планирования и дискуссий. Несколько месяцев я проверял github чаще, чем почту или фейсбук. Github был моим фейсбуком (только без милых котиков). Если вы не знаете о git и подобных вещах, но пишете научные статьи, настоятельно рекомендую изучить системы контроля версий ^[7]. Изучение такой системы принесет пользу даже если вы пишете статью в одиночку, кроме того, вы сможете снимать красивые видео ^[8] о том, как создавалась статья.

Что важнее, тот дух совместного творчества, заполнивший нашу команду в Институте перспективных исследований ^[9], по-настоящему поразителен. Мы не разбивались на группы. Мы разговаривали, делились идеями, объясняли друг другу разные вещи ^[10], и совершенно забыли, кто что сделал (нам даже пришлось приложить некоторое усилие для восстановления истории событий, которая в противном случае канула бы в лету). Результатом явилось существенное увеличение продуктивности. Урок, который можно отсюда извлечь (помимо того, что Институт перспективных исследований — первоклассный исследовательский институт), состоит в том, что математикам идет на пользу, когда они не чувствуют себя такими уж собственниками по отношению к своим идеям. Я знаю, знаю, карьера в академии зависит от того, насколько правильно распределены вознаграждения за вклад в работу, но на самом деле это всего лишь неприятная особенность нашего времени. Если бы научить математиков делиться наполовину готовыми идеями и не заботиться о том, кто сделал какой вклад в работу, или даже кто авторы работы, мы бы достигли нового, невообразимого ранее уровня продуктивности. Прогресс совершают те, кто посмел нарушить правила.

По-настоящему открытую среду не ограничивают копирайт, жадные до наживы издатели, патенты, коммерческие секреты и схемы финансирования, основанные на ошибочных мерках достижений. К сожалению, мы все существуем внутри системы, страдающей всеми из перечисленных зол. Но мы сделали небольшой шаг в правильном направлении, сделав исходный код открытым ^[11] под лицензией Creative Commons. Кто угодно может изменять книгу, присылать нам исправления и улучшения, переводить её или даже продавать, не делясь с нами прибылью. (Если вы слегка наморщились, читая последнее предложение, вы уже часть системы.)

Мы решили не прибегать к помощи академических издателей, потому что хотели сделать книгу доступной для всех быстро и бесплатно. Книгу можно скачать, а можно дёшево купить в твердом ^[12] или мягком переплете ^[13] на lulu.com ^[14]. (Когда вы в последний раз платили меньше 30$ за 600-страничную академическую монографию в твердом переплете?) Опять же, я чувствую, что некоторые думают «но настоящий академический издатель гарантирует качество». Такой способ мышления ^[15] напоминает о спорах между Википедией и Британникой, и мы все знаем, чем закончилась эта история. Да, мы должны обеспечить качество. Но как только мы осознаем до конца, что кто угодно может опубликовать что угодно в интернете на обозрение всему миру, и может сделать из этого дешёвую книгу, которая выглядит профессионально, мы сразу поймем, что критика как инструмент больше не эффективна. Вместо этого нам нужна децентрализованная система эндорсмента (рекомендаций — прим.), которая бы не работала в интересах небольшой группы людей. Ситуация постепенно движется в этом направлении, например, с недавним появлением Selected Papers Network ^[16] и похожими инициативами. Надеюсь, всё это получит широкое распространение.

Однако, есть еще кое-что, что мы можем сделать. Что-то более радикальное, но в то же время более полезное. Вместо того чтобы только позволять людям оценивать статьи, почему бы не разрешить им участвовать? Выложите все свои статьи на github и разрешите другим обсуждать их, делать ответвления, улучшать их и отправлять вам поправки. Звучит как бред сумасшедшего? Конечно, open source тоже звучало как бред, когда Ричард Столлман только опубликовал ^[17] свой манифест. Давайте честно, кто будет красть ваши LaTeX исходники? Для воровства есть много других гораздо более ценных вещей. Если вы профессор с постоянным контрактом, вы можете позволить себе быть первопроходцем. Попросите вашего аспиранта научить вас использовать git и выложите в открытый доступ ваши работы. Не бойтесь, постоянный контракт вам дали как раз для того, чтобы вы могли делать подобные вещи.

Итак, приглашаем всех помочь нам с улучшением книги на github. Вы можете оставлять комментарии, указывать на ошибки и, более того, самостоятельно их исправлять! Нам не важно, кто вы, насколько большой вклад внесёте и кто присвоит себе заслугу за ваш вклад. Единственное, что имеет значение, — есть ли в вашем вкладе какая-нибудь ценность.

Мое последнее наблюдение — о формализации математики. Математикам нравится думать, что их статьи можно в принципе формализовать в теории множеств. Эта мысль даёт им ощущение безопасности, не сильно отличающееся от чувства, которое испытывает набожный человек, заходя в почтенный храм. Гомотопическая теория типов является основаниями математики, представляющими альтернативу теории множеств. Мы тоже утверждаем, что обычная математика может быть в принципе формализована в нашей теории. Но, знаете что, вам не нужно верить нам на слово! Мы формализовали наиболее сложные части нашей книги по HoTT и проверили доказательства с помощью proof assistants. Не единожды ^[18], а дважды ^[19]! Мы сначала формализовали, а затем написали книгу, потому что формализовывать оказалось проще. Мы победили по любому счету (если предполагать, что было какое-то соревнование).

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

Автор: TheHottie

Источник ^[20]