Перевод статьи Андрея Бауера — The HoTT book
Книга по HoTT закончена!
Начиная с весны, и даже раньше, я участвовал в командном проекте по написанию книги по гомотопической теории типов (Homotopy Type Theory). Она наконец написана и готова к употреблению. Вы можете скачать книгу бесплатно: homotopytypetheory.org/book/. Майк Шульман рассказал о содержании книги, так что я не буду повторять то же самое. Вместо этого я бы хотел прокомментировать некоторые социо-технологические аспекты создания книги и, в частности, рассказать о том, чему нас научило сообщество Open source.
Мы — две дюжины математиков, написавших 600-страничную книгу меньше чем за полгода. Это впечатляет, поскольку обычно математики не работают большими группами. В маленькой группе математики могут позволить себе использовать устаревшие технологии — например, пересылать друг другу исходники LaTeX по электронной почте, — но когда математиков больше двадцати, их не спасает даже Dropbox. К счастью, многие из нас — специалисты по Computer Science, замаскированные под математиков, так что мы знали, как справиться с логистикой. Мы использовали git и github.com. Потребовалось время, чтобы привыкнуть, но никаких реальных сложностей не возникло. В конце репозиторий стал не только архивом для наших файлов, но также центральным хабом для планирования и дискуссий. Несколько месяцев я проверял github чаще, чем почту или фейсбук. Github был моим фейсбуком (только без милых котиков). Если вы не знаете о git и подобных вещах, но пишете научные статьи, настоятельно рекомендую изучить системы контроля версий. Изучение такой системы принесет пользу даже если вы пишете статью в одиночку, кроме того, вы сможете снимать красивые видео о том, как создавалась статья.
Что важнее, тот дух совместного творчества, заполнивший нашу команду в Институте перспективных исследований, по-настоящему поразителен. Мы не разбивались на группы. Мы разговаривали, делились идеями, объясняли друг другу разные вещи, и совершенно забыли, кто что сделал (нам даже пришлось приложить некоторое усилие для восстановления истории событий, которая в противном случае канула бы в лету). Результатом явилось существенное увеличение продуктивности. Урок, который можно отсюда извлечь (помимо того, что Институт перспективных исследований — первоклассный исследовательский институт), состоит в том, что математикам идет на пользу, когда они не чувствуют себя такими уж собственниками по отношению к своим идеям. Я знаю, знаю, карьера в академии зависит от того, насколько правильно распределены вознаграждения за вклад в работу, но на самом деле это всего лишь неприятная особенность нашего времени. Если бы научить математиков делиться наполовину готовыми идеями и не заботиться о том, кто сделал какой вклад в работу, или даже кто авторы работы, мы бы достигли нового, невообразимого ранее уровня продуктивности. Прогресс совершают те, кто посмел нарушить правила.
По-настоящему открытую среду не ограничивают копирайт, жадные до наживы издатели, патенты, коммерческие секреты и схемы финансирования, основанные на ошибочных мерках достижений. К сожалению, мы все существуем внутри системы, страдающей всеми из перечисленных зол. Но мы сделали небольшой шаг в правильном направлении, сделав исходный код открытым под лицензией Creative Commons. Кто угодно может изменять книгу, присылать нам исправления и улучшения, переводить её или даже продавать, не делясь с нами прибылью. (Если вы слегка наморщились, читая последнее предложение, вы уже часть системы.)
Мы решили не прибегать к помощи академических издателей, потому что хотели сделать книгу доступной для всех быстро и бесплатно. Книгу можно скачать, а можно дёшево купить в твердом или мягком переплете на lulu.com. (Когда вы в последний раз платили меньше 30$ за 600-страничную академическую монографию в твердом переплете?) Опять же, я чувствую, что некоторые думают «но настоящий академический издатель гарантирует качество». Такой способ напоминает о спорах между Википедией и Британникой, и мы все знаем, чем закончилась эта история. Да, мы должны обеспечить качество. Но как только мы осознаем до конца, что кто угодно может опубликовать что угодно в интернете на обозрение всему миру, и может сделать из этого дешёвую книгу, которая выглядит профессионально, мы сразу поймем, что критика как инструмент больше не эффективна. Вместо этого нам нужна децентрализованная система эндорсмента (рекомендаций — прим.), которая бы не работала в интересах небольшой группы людей. Ситуация постепенно движется в этом направлении, например, с недавним появлением Selected Papers Network и похожими инициативами. Надеюсь, всё это получит широкое распространение.
Однако, есть еще кое-что, что мы можем сделать. Что-то более радикальное, но в то же время более полезное. Вместо того чтобы только позволять людям оценивать статьи, почему бы не разрешить им участвовать? Выложите все свои статьи на github и разрешите другим обсуждать их, делать ответвления, улучшать их и отправлять вам поправки. Звучит как бред сумасшедшего? Конечно, open source тоже звучало как бред, когда Ричард Столлман только опубликовал свой манифест. Давайте честно, кто будет красть ваши LaTeX исходники? Для воровства есть много других гораздо более ценных вещей. Если вы профессор с постоянным контрактом, вы можете позволить себе быть первопроходцем. Попросите вашего аспиранта научить вас использовать git и выложите в открытый доступ ваши работы. Не бойтесь, постоянный контракт вам дали как раз для того, чтобы вы могли делать подобные вещи.
Итак, приглашаем всех помочь нам с улучшением книги на github. Вы можете оставлять комментарии, указывать на ошибки и, более того, самостоятельно их исправлять! Нам не важно, кто вы, насколько большой вклад внесёте и кто присвоит себе заслугу за ваш вклад. Единственное, что имеет значение, — есть ли в вашем вкладе какая-нибудь ценность.
Мое последнее наблюдение — о формализации математики. Математикам нравится думать, что их статьи можно в принципе формализовать в теории множеств. Эта мысль даёт им ощущение безопасности, не сильно отличающееся от чувства, которое испытывает набожный человек, заходя в почтенный храм. Гомотопическая теория типов является основаниями математики, представляющими альтернативу теории множеств. Мы тоже утверждаем, что обычная математика может быть в принципе формализована в нашей теории. Но, знаете что, вам не нужно верить нам на слово! Мы формализовали наиболее сложные части нашей книги по HoTT и проверили доказательства с помощью proof assistants. Не единожды, а дважды! Мы сначала формализовали, а затем написали книгу, потому что формализовывать оказалось проще. Мы победили по любому счету (если предполагать, что было какое-то соревнование).
Надеюсь, книга вам понравится, она содержит поразительное количество новой математики.
Автор: TheHottie
