Two dozen mathematicians wrote a 600 page book in 6 months on GitHub
math.andrej.com
math.andrej.com
"However, there is something else we can do. It is more radical, but also more useful. Rather than letting people only evaluate papers, why not give them a chance to participate and improve them as well? Put all your papers on github and let others discuss them, open issues, fork them, improve them, and send you corrections. Does it sound crazy? Of course it does, open source also sounded crazy when Richard Stallman announced his manifesto.
Let us be honest, who is going to steal your LaTeX source code? There are much more valuable things to be stolen. If you are tenured professor you can afford to lead the way. Have your grad student teach you git and put your stuff somewhere publicly. Do not be afraid, they tenured you to do such things."
This is a fascinating idea. I'm curious. If we did this (say, with an upcoming technology paper), would anyone want to contribute?
rms: "Aaaaaaaaaaaaaarrrrrrrrrrrrggggggggghhhhhhhhhhhhhhhhhh"
(Background: http://www.gnu.org/philosophy/open-source-misses-the-point.h...)
PS: I hate the stupid fights over words: "Gnu/Linux", "Free software"... It's called "Linux" and it's called "open source software". Now get off my lawn.
He doesn't sound crazy he is just very eccentric as a individual. And he has an "extremist" position, some would say. IMHO we need someone like that to keep us honest. Remember all the years people like Microsoft put actually money into discrediting FOSS? Would a wishy washy attitude have done much good then? Diplomacy doesn't work worth a damn when your enemy wants to destroy you by any means possible, be it by embracing you or extinguishing you
After this NSA scandal broke, I feel I was a little quick to judge him. I'm not going to give up my cellphone, but I've already quit using FB and have started using more digital privacy tools like OTR in pidgin.
I haven't heard an argument for "GNU/Linux" that's any more than "hey a bunch of GNU code is part of linux so GNU should be in the name." which seems a much less principled objection. If I'm wrong though, I'd love to be corrected.
So I suppose you are right, it is a much less principled objection :)
[incidentally, it's the official post announcing the book]
"But more importantly, the spirit of collaboration that pervaded our group at the Institute for Advanced Study was truly amazing. We did not fragment. We talked, shared ideas, explained things to each other, and completely forgot who did what (so much in fact that we had to put some effort into reconstruction of history lest it be forgotten forever). The result was a substantial increase in productivity. There is a lesson to be learned here (...), namely that mathematicians benefit from being a little less possessive about their ideas and results. I know, I know, academic careers depend on proper credit being given and so on, but really those are just the idiosyncrasies of our time. If we can get mathematicians to share half-baked ideas, not to worry who contributed what to a paper, or even who the authors are, then we will reach a new and unimagined level of productivity. Progress is not made by those who break rules."
"Truly open research habitats cannot be obstructed by copyright, profit-grabbing publishers, patents, commercial secrets, and funding schemes that are based on faulty achievement metrics. Unfortunately we are all caught up in a system which suffers from all of these evils. But we made a small step in the right direction by making the book source code freely available under a permissive Creative Commons license. Anyone can take the book and modify it, send us improvements and corrections, translate it, or even sell it without giving us any money. (If you twitched a little bit when you read that sentence then the system has gotten to you.)"
(borrowing the google cache link from below: https://webcache.googleusercontent.com/search?strip=1&q=cach...)
to the parent - by now, man, you probably know that a lot of people with downvoting karma here do lack a sense of humor and/or have very low tolerance for sarcasm. The main impact of XML innovation on human civilization is the ability to use <sarcasm> in an environment like this to at least minimize the wrath of the former group. Nothing though can help with the latter.
Until you do, don't assume the set of things women are inherently suitable for/interested in/able to do is not the same as for men.
Male and female brains have been known to be physically different for quite a while. How much of an impact this has on thought process I don't know.
Every time someone mentions that they think there's a difference between males and females, someone pushes up their glasses and asks "source?", as if the 6th layer of comments on a news aggregater is the place to rehash decades of complicated studies and biology.
Accept that the position that there are some differences is a reasonable one and move on, even if you disagree. We don't know how much of it is mental, but we don't know much about "mental" at all right now. We're guessing based on what we do know.
Just as long as we all don't let our guesses about the unknowns of science cloud our judgment in specific, concrete situations, we'll be perfectly fine. And merely believing that some differences do exist won't itself cause that.
Accepting that there are some differences does not lift the burden of persuasion off those who assert the existence of a particular difference, in the same way that accepting the idea that there are some murderers in the world doesn't lift the burden of persuasion off those who insist that a particular person is a murderer.
There are also a lot of difference in socialization and social treatment that are not innate differences.
> It is valid to conjecture that perhaps the observed difference is due to one of the innate differences.
It is also valid to conjecture that perhaps the observed difference is due to cultural/environmental forces and not due to one of the innate differences.
There's a big gap between conjecturing that something may perhaps be true (which is a very weak position that doesn't require much support) and asserting that something it true, or probably true, or the best explanation given the available evidence.
It is. But we originally started with someone conjecturing that it wasn't, and getting told off for it. Don't change it from "believing X is reasonable" to "believing not X is also reasonable".
Do you have proof for this assertion?
We know there are differences. We've chipped away at it for decades, and no one in science disagrees. The problem is that the obvious differences that are manifested are all macro physical, we don't know how the differences extend to the mental area. But then, in these kinds of arguments we don't really even know what we mean by "mental" because, technically, it's all physical. (At least, the part science cares about.)
Some people think that it doesn't extend to "mental". Some do. Considering the basic fact that our mental states are very obviously modified chemically, and that males and females get different chemical influences throughout life, I can't think anything but we have to leave that possibility open that there are consistent developmental differences. This is not one of those situations where it's probably most accurate to assume there is no difference until one is proven.
Also, stonemetal posted a link elsewhere in this comment thread. No one wanted to reply to that, they just wanted to post "are you sure?" in this thread.
And I can't help but wonder if this is supposed to be satire, considering above I posted:
> Every time someone mentions that they think there's a difference between males and females, someone pushes up their glasses and asks "source?", as if the 6th layer of comments on a news aggregater is the place to rehash decades of complicated studies and biology.
http://hottheory.files.wordpress.com/2013/03/hott-online.pdf
http://hottheory.files.wordpress.com/2013/03/hott-ebook.pdf
First commit in Nov '12. Most work seems to be have been done since Jan/Feb '13:
As for the work itself, great stuff, I look forward to reading it, or at least dipping into it (not a mathematician).
If you've got a directory system that goes many levels deep though those long file/folder names won't fit on your screen and so you can't see at glance where things at.
I do sympathize with your plight though, I guess I've just accepted that if I want to find something I download again I have to rename or move it to where it ought to belong.
It also has a feature which allows you to rename the PDF based on the bibliographic reference it creates.
Using those two together has been a really easy way to earn brownie points with my professor boss.
This article is a start, but it would probably be stronger if the author had a nuts-and-bolts tutorial about how to use Git from the point of view of someone whose use case involves LaTeX markup rather than source code.
If you could provide a use case to demonstrate how Git+latex is a winner, I'd genuinely appreciate it!
Edit: As soon as I submitted this it occurred to me that for collaborative editing Git is the obvious choice.
You can somewhat improve the situation if you adopt a somewhat weird source-formatting policy, where you write each sentence on one separate long-ish line, rather than flowing by paragraph. Then you will be able to automatically merge as long as nobody has made an edit or move that touches the same sentence, giving you better merge granularity. But even then conflicts happen pretty often, and few people like this style of formatting (maybe it'd work better with tool support).
For a book this might work better, though, because I assume you'd be making less frequent edits, and people would less often be working at the same time.
As stated above, Dropbox doesn't even try to merge files, but Git does, which is definitely an advantage (at the very least, it tells you where the conflicts are, which is far more reliable than trying to work out the conflicts by hand, or with a separate diffing tool).
Merging. People can work on the manuscript at the same time, and as long as they edited non-overlapping regions, git will merge both contributions silently and painlessly.
Editing a word processor document stored in a shared Dropbox folder, I guess you'd need to inspect both new versions and do the merge manually?
edit: just saw your edit :)
Particularly with the fuzzy temporal revs thing, e.g. HEAD@{1 week ago}
Merges: Git does all the bookkeeping for collaboration -- if you have two people making changes, it's much easier to merge them with VCS. Or an independent contributor can use rebase to, as the manual page succinctly puts it, "forward-port local commits to the updated upstream head."
Discussion: If you use a Web-based product like Github or Gitlab (an open-source, self-hostable GitHub clone), you get an issue tracker and a dedicated discussion thread for individual changes.
The is that there is now an expansive, informal/readable, and machine verified writeup of homotopy type theory.
"Nicolas Bourbaki is the collective pseudonym under which a group of (mainly French) 20th-century mathematicians wrote a series of books presenting an exposition of modern advanced mathematics, beginning in 1935."
It's better than anything I've read from any mathematician. They seem to forget that people don't know what they are talking about to start with.
I quite like this book that you linked, BTW.
Drop me a line toni@banyan.co if you want early access.
"Homotopy Type Theory is a recent advancement in the area of dependent types. Think Agda, Coq, Idris-style languages if you're familiar with them... otherwise think GADTs on supersteroids gone berserk.
Dependent types allow you to be extremely precise with your data types. You can talk about not just lists or lists of strings.... but also lists of strings of length n (for some natural number n). In the far future, it may be the key to getting fast-as-C performance (think removing bounds checking on arrays completely safely) and software verified correctness of a program simultaneously.
This isn't software, though. This is a math book. There was a realization a few years ago that equality types (the ability to express x = y in the type system) gave rise to a mathematical structure called a weak ω-groupoid which was giving homotopy and category theorists a hard time. Homotopy Type Theory (HoTT) is a typed lambda calculus that makes studying these things easier. In fact, every data type corresponds to (a very boring) weak ω-groupoid.
What this allows mathematicians to do, though, is to create new interesting data types corresponding to more interesting examples of these things. You get a data type for a Circle, or a Sphere, or a Torus. You can define functions between them via recursion the same way you'd define a function on lists or trees. These new fancy data types are called higher inductive types, and while they don't (currently) have any use for programmers, they pay the meager salaries of long beards in the ivory tower.
The other novelty of the theory might be more interesting for programmers some day (at least if you believe dependent types will save the world).
A guy named Voevodsky proposed a new axiom called the Univalence Axiom that makes HoTT a substatial alternative to the former foundations of mathematics. The Univalence Axiom formalizes a practice mathematicans had been using for a long time, (despite its technical incompatibility with ZFC). tl;dr, the Univalence Axiom says that if two data types are isomorphic then they are equal.
Eventually, this axiom may allow a programmer to do some neat things. For instance, a programmer could write two versions of a program -- a naive version and a "fast" version. (Currently, all programmers only write the "fast" version). If you want to formally prove your "fast" program doesn't suck, it's nasty. However, it might even be humanly possible to prove some correctness about the naive version. The Univalence Axiom (once given "computational semantics") may be able to let us prove things about the dumb, slow, reference implementation of a program or library, then transfer that proof of correctness to the fast one.
To give a small example for anyone familiar with a dependently-typed language, you may notice that in Coq and Agda and whatever, the first data type you learn (and one you stick with for a long time) are the unary natural numbers. That is, you have 0, and 0+1, and 0+1+1, and 0+1+1+1, etc.. We use unary numbers because they are reaaaally easy to prove stuff about. But as any programmer might guess, actually doing anything with them is suicide. The Univalence Axiom would allow us to keep on working with unary numbers for all of our proofs, but then swap them out for actual, honest-to-God 2's complement representations when it comes time to run the program.
So there's that.
Not everyone cares about software correctness, though. But if you're sold on category theory, here's a neat trick. You probably know that equality becomes a hairy, nasty thing in category theory. Two objects can be equal or isomorphic. If you move onto 2-categories, two categories can be equal, isomorphic, or equivalent! And for higher category theory, you end up with even more notions of equaltiy, isomorphism, equivalence, etc, etc.
In a univalent foundation of category theory (which appears in the later chapters of this book), we see that all of these notions of equality collapse down into just one. If two things are isomorphic, then they are, by definition, equal to each other. You no longer have to worry about that stupid squiggle over your equals signs, because univalence means that every construction must respect the structure of your data. There are no leaky abstractions in your data types!"
[1] http://www.reddit.com/r/haskell/comments/1gr3uw/the_homotopy...
I can think of many sets of notes on the MIT OCW site that are CC, which I'd like to be able to modify and share but can't because the source is missing.
Anyone else have thoughts on the right license for this sort of project?
I was really fascinated by some of his older blog publications (and I was only scratching the surface):
http://math.andrej.com/2007/09/28/seemingly-impossible-funct... (by Martin Escardo, an article about a Haskell program doing exhaustive search over the “Cantor space” of infinite sequences)
http://math.andrej.com/eff/ (Language Eff, a functional programming language based on algebraic effects and their handlers.) My understanding is that in this language all effects and evaluation order are explicit; effects and pure functions are easily and explicitly composable. Something like monads but more advanced. (My interpretation is probably wrong!)
http://andrej.com/plzoo/ (The Programming Language Zoo). A number of mini languages which demonstrate various techniques in design and implementation of programming languages. (calculator, mini-ML, mini-Haskell, mini-Prolog, etc)
But sometimes it's hard to encourage VC simply because it shifts the balance of power. You can't hold anyone hostage with "your" code. Mistakes are traceable. You can't waste as much time in meetings, discussing things like project status and interfaces. Silos exist for a reason, it's just not a good reason.
:) I think we need a new verb here.
Note that this hasn't been updated in 13 years. The gold that has been lost since then truly saddens me.
Really nice to have the source.
So what you actually want to do is put a line break after every sentence and possibly after every clause, so that in the LaTeX source diffs work sanely, while the output looks as normal.
What you'd like Git (or whatever your diff'ing program) to do is parse the individual sentences as individual lines for version control.
To each his own though. I have trained myself to start putting LaTeX sentences on separate lines to accomodate for this, but don't think that this is the best solution.
It'd be nice to have an intermediate step that turned your LaTeX into a canonical form that works well with Git. And then when you are about to edit, converts it back into a nice-looking 80-column text file, or whatever you prefer.