I wasn’t aware that mathematicians are able to collaborate en masse on proofs now with Lean just like software engineers can make 10 pull requests to the same file in a day.
That’s the main thing that Tao identifies that Lean enables, collaboration where Lean does the work of checking the output of the collaborator, thus becoming a force multiplier. There’s still the issue of how the proof should be organized, how it should be factored into various implications, and here, like in the Linux kernel, contributors with seniority referee the process, as Tao did with his “experiment”.
reply