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

Перевод статьи Андрея Бауера — 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. Не единожды, а дважды! Мы сначала формализовали, а затем написали книгу, потому что формализовывать оказалось проще. Мы победили по любому счету (если предполагать, что было какое-то соревнование).

Надеюсь, книга вам понравится, она содержит поразительное количество новой математики.
Поделиться публикацией
Комментарии 35
    +5
    Остаётся только надеяться, что и другие авторы последуют их примеру.
      0
      Для чего HoTT? Что в перспективе? Писать программы вместо доказательств?
        +13
        Для минусующего (в том числе карму) стада, которому что-то там померещилось, и почему-то воспринимающем мои вопросы как «нафига Haskell, если есть Basic», и которое является, по-видимому, знатоком HoTT в третьем поколении, позвольте дать более развернутый вопрос от новичка, впервые прочитавшем о HoTT.

        Является ли HoTT, как основание математики «не на множествах», мостом к автоматизации математических доказательств? На упомянутом в статье языке Agda, если я правильно понял, эти вещи уже частично делаются.

        (мои познания в HoTT ограничены только этим постом, и по этому поводу найденной шикарной статьёй про «Но ведь это одно и то же» 2*9 и 9*2, половину которой слёту неосилил, это действительно — новая математика)
          +11
          Возможно, следующий отрывок интервью Владимира Воеводского (кстати говоря, лауреата Филдсовской премии), в котором он описывает историю создания HoTT, поможет понять, зачем нужна эта теория и что вообще происходит:

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

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

          Я был очень хорошо знаком с этой проблемой и думал о ней еще в 1989 году, когда Миша Капранов и я работали над теорией поли-катергорий. Тогда нам казалось, что ее решить невозможно. То, что мне удалось понять в 2005 году, скомбинировав идеи теории гомотопий (части современной топологии) и теории типов (части современной теории языков программирования), было совершенно удивительно, и открывало реальные возможности построения того самого языка, на котором люди могут писать доказательства, которые сможет проверять компьютер. Дальше был большой перерыв в моей математической деятельности.
          [...] К идеям, связанным с компьютерной проверкой доказательств, я вернулся только летом 2009, когда мне стало окончательно ясно, что с исторической генетикой ничего не получается. И буквально через несколько месяцев случились два события, которые продвинули эти идеи от общих наметок, над которыми, я думал, придется работать еще не один год, до стадии, на которой я смог заявить, что я придумал новые основания математики, которые позволят решить проблему компьютерной проверки доказательств. Сейчас это называется «унивалентные основания математики» и ими занимаются как математики, так и теоретики языков программирования. Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут «понимать» компьютеры можно считать в основном решенной. [...] Первые примеры языков того класса с которыми я работаю, были созданы в конце 1970-ых и известны под названием «Martin-Lof type theories». Удивительным образом языки были, программные системы использующие эти языки создавались и даже становились популярными (особенно система «Coq» которую создали французы), но понимания того, о чем эти языки позволяют говорить, не было. Получалось, что используется только очень небольшая часть возможностей языка, та, которая, как теперь ясно, позволяет говорить про множества. Язык же в целом позволяет говорить про гомотомические типы любого уровня сложности. Разрыв, как ты понимаешь, огромный. Как следствие сами языки не совершенствовались, потому что было не ясно, что можно менять, а что нельзя. Теперь, когда мы понимаем, что в этих языках существенно, а что нет, открывается возможность сделать их значительно более «мощными» и, как следствие, более удобными для практического использования.
            –1
            Спасибо!
            Но насчет замены оснований математики — с этим трудно согласиться.
              0
              Важно понимать, что множества сами по себе никуда не денутся. Замена, о которой говорит Воеводский, происходит на более низком уровне: связка «логика первого порядка + аксиомы ZFC» заменяется на HoTT. Считается, что аксиомы ZFC работающих математиков всё равно не интересуют (кроме специалистов по логике), и в современном виде необходимая математикам теория множеств гораздо лучше формализуется с помощью ETCS.

              ETCS инспирирована теорией категорий (но не базируется на ней): в качестве базовых объектов берутся функция и множество (в ZFC базовые объекты — множество и элемент множества), и элементы множества A в ETCS определяются как функции из фиксированного одноэлементного множества в множество A (т.к. эти функции взаимно-однозначно соответствуют элементам A), а «одноэлементность» в свою очередь можно определить как свойство множества иметь ровно одну функцию из любого множества в себя. Подробное изложение для нематематиков можно найти здесь: arxiv.org/abs/1212.6543 Там же можно узнать, почему математики не используют ZFC (например, потому, что число пи в этой системе аксиом является множеством).

              В HoTT в свою очередь можно строить объекты, которые работают ровно так, как те штуки, которые описывает ETCS. Эти штуки в HoTT называются множества.
                0
                т.е. если математика — это химия, текущие основания математики (на множествах) — это атомы, то HoTT — это элементарные частицы, которыми можно описать основания математики, и которые позволяют более точно (т.к. оперируют более фундаментальными понятиями) работать с математикой?
                  0
                  Судя по нику, вы являетесь явным поклонником HoTT.

                  Спасибо за отрывок из интервью, стало понятней.
                  0
                  Если я правильно понял, то на пальцах эту теорию можно объяснить так: в нынешнем основании много аксиом, а новое основание превращает их в теоремы и доказывает исходя из меньшего числа аксиом, при этом новое открывает новые возможности, но на текущей математики они не отразятся. Или, аналогия, Математика — язык, компилятор которого написан на Си, нынешнее основание — сам Си, а новое — ассемблер :)
              +5
              Не являюсь профессиональным математиком, чтобы судить, но на первый дилетансткий взгляд — отличная новая теория, берущаяся за основания математики с неожиданной стороны.
              Вот тут можно прочесть краткую историческую справку, чтобы понять, зачем она вообще нужна.
              А вот тут — пояснение, что именно в ней нового и чем она отличается от ОТТ.
                –1
                Интересно как была организована работа. Какие были соглашения, учитывающие специфику git — он всё же на строки ориентирован, а книга вещь такая — слово вставил и все строки полезли.
                  –2
                  Предполагаю, что за вёрстку самой книги, кто-то отвечал отдельно. Но это идея для отличного нового сервиса, что-то вроде вики, но сразу на основе полиграфических шаблонов, у Adobe, возможно, уже что-то в этом роде есть.
                    +11
                    man tex
                    man latex
                      0
                      У меня уже после комменты мысль мелькнула, что что-то вроде html использовалось. Жаль — путь не для всех.
                        +1
                        для всех причастных к науке, это точно
                          0
                          Причем тут наука? Меня интересовала методология совместной работы над книгами вообще.
                            +2
                            я про latex имею в виду. В мире исследований математики\программирования его положено знать.

                            А про методологию совместной работы у меня создаётся впечатление, что её и не было вовсе — кроме той, что подразумевается гитхабом
                              –4
                              Я в курсе. В принципе вы на вопрос ответили, правда в несколько неприятной форме.

                              Методология и задавалась связкой git и latex (хотя на его месте мог быть любой другой язык логической разметки, в котором переводы строк и прочее форматирование если и есть, то не приветствуется, например html). В диффах были видны целые замененные абзацы, в исходниках представляемые одной строкой, а при хорошем инструменте показывались буквы/слова/предложения.

                              Просто я надеялся, что можно как-то обойтись без языка разметки (или его не видеть под TUI/GUI) и при этом комфортно просматривать диффы.
                                0
                                Диффы в git смотреть вполне комфортно)
                                  –2
                                  Обычного текста, разбитого на строки ентерами?
                    +2
                    ...
                    private
                      ℕ-get-S : ℕ → ℕ
                      ℕ-get-S 0 = 42
                    ...
                    

                    Действительно, очень важная константа для описания множества целых чисел.
                      +1
                      Интересно а что дали исследования по основаниям математики в прикладнеом аспекте, их значение для прояснения здания математики я не оспариваю
                        +14
                        > «Github был моим фейсбуком (только без милых котиков)»
                        Очень даже с котиками!
                          +8
                          Осьмикотиками!
                          +6
                          классно, в книге есть справочник символов. Как же я ненавидел, когда в учебнике по матану внезапно появлялся какой-нибудь крючок, который автор не удосуживался объяснить!
                            +6
                            Заказал в твёрдом переплёте. Хоть и уверен, что ничего не пойму в этой книге, но такие проекты надо поддерживать.
                              +5
                              Хотелось бы видеть больше книг по современной высшей математике, написанных в более доступной манере. Я уважаю сухой академический стиль, но всё же сложно переоценить простоту и красочность естественного языка при описании абстрактных понятий. Я не имею в виду научно-популярные труды вроде книг Брайана Грина, в которых вообще нет формул. Ведь мой опыт чтения книг по программированию показывает, что даже сложные практические концепции можно наглядно продемонстрировать и пояснить. Также с большим теплом вспоминаю книги вроде «Наглядная геометрия и топология» и издания «Кванта»…

                              Спасибо за ваш труд, постараюсь выделить время и полистать вашу книгу.
                                0
                                Интересно, как они работу распределяли. Когда каждый пишет свою главу — все достаточно просто. Кажется достаточно сложным мержить изменения одного файла — что бы правки разных людей не приводили к стилистическим ошибкам.
                                  +1
                                  А планируется ли создание какого-нибудь proof assistants, основанного на HoTT? Мне, как пользователю Coq, очень интересно.
                                  0
                                  >Вместо этого нам нужна децентрализованная система эндорсмента (рекомендаций — прим.)
                                  Endorsement – это скорее поощрение, чем рекомендация.

                                  А статья интересная. И видео тоже занимательное :)
                                    0
                                    Мне кажется движок вроде MediaWiki (с установленным Math extension) лучше бы подошел для этой цели. Хотя признаюсь честно с GitHub знаком весьма поверхностно.
                                      0
                                      А как сливать изменения в итоговой версии от распределенной команды разработчиков? Как следить за историей изменений и в случае ошибки откатывать версии?

                                      ИМХО, пример работы, описанный в этом посте, раскрывает сильные стороны распределенных систем контроля версий.
                                        0
                                        В MediaWiki есть история версий. И довольно удобный просмотр изменений между ними. Откат к конкретной версии тоже есть. Работа через вебинтерфейс или клиент.
                                      0
                                      А как бы вот теперь всё это перевести бы на много языков, включая русский, и поддерживать в актуальном состоянии?

                                      Желательно, средствами всё того же github-а…

                                      Только полноправные пользователи могут оставлять комментарии. Войдите, пожалуйста.

                                      Самое читаемое