Un livre sur la théorie homotopique des types vient d’être publié par des mathématiciens. A priori ça ne concerne que les spécialistes du sujet…
Et pourtant ça concerne tout le monde, tant sa conception originale et les leçons qui en sont tirées ci-dessous ont valeur d’exemplarité.
Du Libre à tous les étages (LaTeX, Creative Commons By-Sa…) mais surtout dans son état d’esprit de partage et de collaboration. Un projet et un article passionnants, à faire lire dans la sphère académique et bien au-delà.
Remarque : Pour commencer, on pourra voir cette courte vidéo « making-of » du livre.
Le livre HoTT
The HoTT book
Andrej Bauer - 20 juin 2013 - Blog personnel
(Traduction : Lgodard, Ilphrin, tcit, Guillaume, igor_d, Yaf, ronanov, fif + anonymes)
Le livre HoTT est terminé !
Depuis le printemps, et même avant, j’ai participé à un super effort collaboratif pour écrire un livre à propos de la Théorie homotopique des types (NdT : HoTT en anglais pour Homotopy Type Theory). Il est enfin terminé et accessible au public. Vous pouvez obtenir le livre librement et gratuitement. Mike Shulman a écrit à propos du contenu de ce livre, donc je ne vais pas répéter cela ici. À la place, je voudrais commenter les aspects socio-technologiques de la création du livre, et en particulier de ce que nous avons appris de la communauté open source sur la recherche collaborative.
Nous sommes un groupe de deux douzaines de mathématiciens qui avons écrit un livre de 600 pages en moins de 6 mois. C’est assez impressionnant, d’autant que les mathématiciens n’ont pas l’habitude de travailler ensemble au sein de grands groupes. Dans un petit groupe ils peuvent s’en sortir en utilisant des technologies obsolètes, comme envoyer aux autres un fichier source LaTeX par email, mais avec deux douzaines de personnes, même Dropbox ou n’importe quel autre système de synchronisation de fichier aurait échoué lamentablement. Par chance, beaucoup d’entre nous sont des chercheurs en Informatique déguisés en mathématiciens, donc nous savions comment attaquer les problèmes de logistique. Nous avons utilisé git et github.com.
Au début, il a fallu convaincre les gens, et se faire à l’outil. Malgré tout, cela n’a pas été trop difficile. À la fin, le dépôt sur le serveur n’était pas seulement une archive pour nos fichiers, mais également un point central pour notre planification et nos discussions. Durant plusieurs mois j’ai consulté GitHub plus souvent que mes emails ou Facebook. Github était mon Facebook (sans les petits chats mignons). Si vous ne connaissez rien aux outils comme git mais que vous écrivez des articles scientifiques (ou que vous créez n’importe quel type de contenu numérique) vous devriez vraiment, vraiment vous renseigner sur des systèmes de gestion de versions. Même en tant que seul auteur d’un article, vous allez gagner à apprendre comment en utiliser un, sans même parler des belles vidéos que vous pouvez produire sur la manière dont vous avez écrit votre papier.
Mais de manière plus importante, c’est l’esprit collaboratif qui imprégnait notre groupe à l’Institute for Advanced Study (Princeton) qui était incroyable. Nous ne nous sommes pas éparpillés. Nous avons discuté, partagé des idées, expliqué certains éléments les uns aux autres, et avons totalement oublié qui avait fait quoi (à tel point que nous avons dû faire des efforts pour reconstruire un historique de peur que ce ne soit oublié pour toujours). Le résultat final a été une augmentation considérable de notre productivité.
Il y a une leçon à en tirer (mis à part le fait que l’Institute for Advanced Study est évidemment le meilleur institut de recherche au monde), à savoir que les mathématiciens ont à gagner à devenir un peu moins possessifs vis-à-vis de leurs idées et leurs résultats. Je sais, je sais, une carrière académique dépend de la juste répartition des mérites de chacun et ainsi de suite, mais ce sont seulement les idiosyncrasies de notre époque. Si nous pouvons faire en sorte que les mathématiciens partagent des idées à moitié développées, ne s’inquiètent pas de savoir qui a apporté quelle contribution à un article, ou même qui en sont les auteurs, alors nous atteindrons un nouveau niveau de productivité encore jamais imaginé. Le progrès est le fait de ceux qui osent enfreindre les règles.
Les milieux de recherche vraiment ouverts ne peuvent être gênés par le copyright, les éditeurs qui s’accaparent le profit, les brevets, les secrets commerciaux, et les programmes de financement qui sont basés sur des outils de mesures de réussite défectueux. Malheureusement nous sommes tous coincés dans un système qui souffre de ces maux. Mais nous avons fait un premier pas dans la bonne direction en mettant le code source du livre disponible librement sous une licence permissive Creative Commons (la CC-By-Sa). N’importe qui peut prendre le livre et le modifier, nous envoyer des améliorations et des corrections, le traduire, ou même le vendre sans même nous donner le moindre sou (si cette dernière phrase vous a quelque peu crispé c’est que vous avez été conditionné par le système).
Nous avons décidé de ne pas faire publier le livre par un éditeur académique pour le moment car nous voulions qu’il soit accessible à tous, rapidement et sans frais. Le livre peut être téléchargé gratuitement, ou bien acheté à peu de frais avec une couverture rigide ou souple sur lulu.com (quand avez-vous pour la dernière fois payé moins de 30$ pour une monographie de 600 pages à couverture rigide ?). Une fois de plus, j’entends déjà certaines personnes dire : « oh mais un vrai éditeur universitaire est synonyme de qualité ». Cette façon de penser rappelle les arguments opposant Wikipédia et Britannica, et nous savons tous comment cette histoire s’est terminée. Oui, la bonne qualité de la recherche doit être assurée. Mais une fois que nous acceptons le fait que n’importe qui peut publier n’importe quoi sur Internet permettant au monde entier de le consulter et en faire un livre bon marché à l’air professionnel, nous réalisons rapidement que la censure n’est plus efficace. À la place, nous avons besoin d’un système décentralisé d’approbation qui ne pourrait pas être manipulé par des groupes d’intérêts spéciaux. Les choses sont en train de bouger dans cette direction, avec la création récente du Selected Papers Networks (Réseaux d’écrits sélectionnés) et d’autres projets similaires. J’espère qu’ils auront un bel avenir.
Cependant, il y a quelque chose d’autre que nous pouvons faire. C’est plus radical, mais aussi plus utile. Plutôt que de laisser les gens se contenter d’évaluer les articles, pourquoi ne pas leur donner une chance de participer et aussi d’améliorer ces articles ? Mettez tous vos articles sur GitHub et laissez les autres en discuter, poser des questions, les utiliser comme bases pour leur travail (fork), les améliorer, et vous envoyer des corrections. Est-ce que cela paraît fou? Bien sûr que oui, l‘open source paraissait également une idée folle lorsque Richard Stallman a lancé son manifeste. Soyons honnêtes, qui va vous voler votre code source LaTeX ? Il y a bien d’autres choses de valeur susceptibles d’être volées. Si vous êtes un professeur titulaire vous pouvez vous permettre d’ouvrir le chemin. Faites-vous enseigner git par vos thésards et mettez vos trucs dans un endroit public. N’ayez pas peur, ils vous ont titularisé pour que vous fassiez des choses comme ça.
Donc nous invitons tout le monde à améliorer le livre en participant sur GitHub. Vous pouvez laisser des commentaires, signaler des erreurs, et même mieux, faire des corrections par vous-même ! Nous n’allons pas nous inquiéter de savoir qui vous êtes et combien vous contribuez et qui devrait recevoir les honneurs. La seule chose qui importe est de savoir si vos contributions sont bonnes.
Ma dernière observation est à propos de la formalisation des mathématiques. Les mathématiciens aiment imaginer que leurs publications peuvent en principe être formalisées dans la Théorie des Ensembles. Ceci leur donne un sentiment de sécurité, qui n’est pas différente de celui ressenti par un croyant entrant dans une cathédrale d’âge canonique. C’est une forme de foi professée par les logiciens. La Théorie homotopique des types est un fondement alternatif à la Théorie des Ensembles. Nous revendiquons nous aussi que les mathématiques ordinaires peuvent en principe être formalisées en Théorie homotopique des types . Mais devinez quoi, vous n’avez pas à nous croire sur parole ! Nous avons formalisé les parties les plus complexes du livre HoTT et vérifié les preuves avec des assistants de preuve électroniques. Pas une fois mais deux. Et nous avons formalisé en premier lieu, puis nous avons écrit le livre car c’était plus simple de formaliser. Nous sommes gagnants sur tous les plans (s’il y a une compétition).
J’espère que le livre vous plaira, il contient une impressionnante quantité de mathématiques inédites.
Original post of Framablog.Votez pour ce billet sur Planet Libre.
