A team of mathematicians wrote a 600-page book in six months using GitHub
Translation of an article by Andrey Bauer - The HoTT book
The HoTT book is over!
Since the spring, and even earlier, I participated in a team project to write a book on the homotopy type theory ( Homotopy Type Theory ). It is finally written and ready to use. You can download the book for free: homotopytypetheory.org/book . Mike Schulman spoke about the content of the book , so I will not repeat the same thing. Instead, I would like to comment on some socio-technological aspects of creating a book and, in particular, to talk about what the Open Source community has taught us.
We are two dozen mathematicians who wrote a 600-page book in less than six months. This is impressive because usually mathematicians do not work in large groups. In a small group, mathematicians can afford to use outdated technologies — for example, send LaTeX sources to each other by email — but when there are more than twenty mathematicians, even Dropbox does not save them. Fortunately, many of us are Computer Science specialists disguised as mathematicians, so we knew how to handle logistics. We used git and github.com . It took time to get used to, but no real difficulties arose. At the end, the repository became not only an archive for our files, but also a central hub for planning and discussions. For several months I checked github more often than mail or facebook. Github was my facebook (only without cute cats). If you do not know about git and similar things, but write scientific articles, I strongly recommend to study version control systems . The study of such a system will be useful even if you are writing an article alone, in addition, you can make beautiful videos about how the article was created.
')
More importantly, the spirit of co-creation that filled our team at the Advanced Research Institute is truly astounding. We did not break up into groups. We talked, shared ideas, explained different things to each other , and completely forgot who did what (we even had to make some effort to restore the history of events, which otherwise would have sunk into oblivion). The result was a significant increase in productivity. The lesson to be learned from this (besides the fact that the Advanced Research Institute is a first-class research institute) is that mathematicians benefit when they do not feel that they are proprietary to their ideas. I know, I know, a career in an academy depends on how well the rewards for contributing to work are distributed, but in reality this is just an unpleasant feature of our time. If we could teach mathematicians to share half-ready ideas and not worry about who made what contribution to the work, or even who the authors of the work, we would reach a new, previously unimaginable level of productivity. Progress is made by those who dare to break the rules.
A truly open environment is not limited by copyright, greedy publishers, patents, trade secrets and financing schemes based on erroneous measures of achievement. Unfortunately, we all exist within a system that suffers from all of the evils listed above. But we took a small step in the right direction by making the source code open under a Creative Commons license. Anyone can change the book, send us corrections and improvements, translate it or even sell it without sharing profits with us. (If you frown slightly while reading the last sentence, you are already part of the system.)
We decided not to resort to the help of academic publishers, because we wanted to make the book accessible to everyone quickly and for free. The book can be downloaded, and you can cheaply buy in hardcover or soft binding on lulu.com . (When was the last time you paid less than $ 30 for a 600-page academic monograph in hardcover?) Again, I feel that some people think "but a real academic publisher guarantees quality." This way of thinking reminds us of the controversy between Wikipedia and Britannica, and we all know how this story ended. Yes, we must ensure quality. But as soon as we realize to the end that anyone can publish anything on the Internet for the whole world to view, and can make this a cheap book that looks professional, we will immediately understand that criticism as a tool is no longer effective. Instead, we need a decentralized endorsement system (recommendations - note), which would not work in the interests of a small group of people. The situation is gradually moving in this direction, for example, with the recent appearance of the Selected Papers Network and similar initiatives. I hope all this will be widespread.
However, there is one more thing that we can do. Something more radical, but at the same time more useful. Instead of just allowing people to rate articles, why not allow them to participate? Put all your articles on github and allow others to discuss them, make branches, improve them and send you corrections. Sounds like crazy stuff? Of course, open source also sounded like nonsense when Richard Stallman just published his manifesto. Let's be honest, who will steal your LaTeX sources? There are many other much more valuable things for theft. If you are a professor with a permanent contract, you can afford to be a pioneer. Ask your graduate student to teach you how to use git and share your work. Do not be afraid, they gave you a permanent contract just so that you could do such things.
So, we invite everyone to help us with improving the book on github. You can leave comments, point out errors and, moreover, correct them yourself! It doesn’t matter to us who you are, how big a contribution you will make and who will claim credit for your contribution. The only thing that matters is whether there is any value in your contribution.
My last observation is about the formalization of mathematics. Mathematicians like to think that their articles can in principle be formalized in set theory. This thought gives them a sense of security, not much different from the feeling that a devout person feels when entering a venerable temple. The homotopic theory of types is the basis of mathematics, representing an alternative to the theory of sets. We also argue that ordinary mathematics can in principle be formalized in our theory. But, you know what, you do not need to take our word for it! We formalized the most difficult parts of our book on HoTT and verified the evidence using proof assistants. Not once , but twice ! We first formalized and then wrote the book, because it turned out to be easier to formalize. We won on any account (assuming there was some sort of competition).
I hope you enjoy the book, it contains an amazing amount of new mathematics.
The HoTT book is over!
Since the spring, and even earlier, I participated in a team project to write a book on the homotopy type theory ( Homotopy Type Theory ). It is finally written and ready to use. You can download the book for free: homotopytypetheory.org/book . Mike Schulman spoke about the content of the book , so I will not repeat the same thing. Instead, I would like to comment on some socio-technological aspects of creating a book and, in particular, to talk about what the Open Source community has taught us.
We are two dozen mathematicians who wrote a 600-page book in less than six months. This is impressive because usually mathematicians do not work in large groups. In a small group, mathematicians can afford to use outdated technologies — for example, send LaTeX sources to each other by email — but when there are more than twenty mathematicians, even Dropbox does not save them. Fortunately, many of us are Computer Science specialists disguised as mathematicians, so we knew how to handle logistics. We used git and github.com . It took time to get used to, but no real difficulties arose. At the end, the repository became not only an archive for our files, but also a central hub for planning and discussions. For several months I checked github more often than mail or facebook. Github was my facebook (only without cute cats). If you do not know about git and similar things, but write scientific articles, I strongly recommend to study version control systems . The study of such a system will be useful even if you are writing an article alone, in addition, you can make beautiful videos about how the article was created.
')
More importantly, the spirit of co-creation that filled our team at the Advanced Research Institute is truly astounding. We did not break up into groups. We talked, shared ideas, explained different things to each other , and completely forgot who did what (we even had to make some effort to restore the history of events, which otherwise would have sunk into oblivion). The result was a significant increase in productivity. The lesson to be learned from this (besides the fact that the Advanced Research Institute is a first-class research institute) is that mathematicians benefit when they do not feel that they are proprietary to their ideas. I know, I know, a career in an academy depends on how well the rewards for contributing to work are distributed, but in reality this is just an unpleasant feature of our time. If we could teach mathematicians to share half-ready ideas and not worry about who made what contribution to the work, or even who the authors of the work, we would reach a new, previously unimaginable level of productivity. Progress is made by those who dare to break the rules.
A truly open environment is not limited by copyright, greedy publishers, patents, trade secrets and financing schemes based on erroneous measures of achievement. Unfortunately, we all exist within a system that suffers from all of the evils listed above. But we took a small step in the right direction by making the source code open under a Creative Commons license. Anyone can change the book, send us corrections and improvements, translate it or even sell it without sharing profits with us. (If you frown slightly while reading the last sentence, you are already part of the system.)
We decided not to resort to the help of academic publishers, because we wanted to make the book accessible to everyone quickly and for free. The book can be downloaded, and you can cheaply buy in hardcover or soft binding on lulu.com . (When was the last time you paid less than $ 30 for a 600-page academic monograph in hardcover?) Again, I feel that some people think "but a real academic publisher guarantees quality." This way of thinking reminds us of the controversy between Wikipedia and Britannica, and we all know how this story ended. Yes, we must ensure quality. But as soon as we realize to the end that anyone can publish anything on the Internet for the whole world to view, and can make this a cheap book that looks professional, we will immediately understand that criticism as a tool is no longer effective. Instead, we need a decentralized endorsement system (recommendations - note), which would not work in the interests of a small group of people. The situation is gradually moving in this direction, for example, with the recent appearance of the Selected Papers Network and similar initiatives. I hope all this will be widespread.
However, there is one more thing that we can do. Something more radical, but at the same time more useful. Instead of just allowing people to rate articles, why not allow them to participate? Put all your articles on github and allow others to discuss them, make branches, improve them and send you corrections. Sounds like crazy stuff? Of course, open source also sounded like nonsense when Richard Stallman just published his manifesto. Let's be honest, who will steal your LaTeX sources? There are many other much more valuable things for theft. If you are a professor with a permanent contract, you can afford to be a pioneer. Ask your graduate student to teach you how to use git and share your work. Do not be afraid, they gave you a permanent contract just so that you could do such things.
So, we invite everyone to help us with improving the book on github. You can leave comments, point out errors and, moreover, correct them yourself! It doesn’t matter to us who you are, how big a contribution you will make and who will claim credit for your contribution. The only thing that matters is whether there is any value in your contribution.
My last observation is about the formalization of mathematics. Mathematicians like to think that their articles can in principle be formalized in set theory. This thought gives them a sense of security, not much different from the feeling that a devout person feels when entering a venerable temple. The homotopic theory of types is the basis of mathematics, representing an alternative to the theory of sets. We also argue that ordinary mathematics can in principle be formalized in our theory. But, you know what, you do not need to take our word for it! We formalized the most difficult parts of our book on HoTT and verified the evidence using proof assistants. Not once , but twice ! We first formalized and then wrote the book, because it turned out to be easier to formalize. We won on any account (assuming there was some sort of competition).
I hope you enjoy the book, it contains an amazing amount of new mathematics.
Source: https://habr.com/ru/post/184716/
All Articles