4 ms·
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
by yo_yo_yo-yo 2y ago
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”.
- ipnon 2y agoNow imagine using Devin on the boring bits! “I remember seeing this proved before but I can’t be bothered to go look it up again.” It’s easy to imagine an explosion of interesting results soon.
- newswasboring 2y ago> I remember seeing this proved before but I can’t be bothered to go look it up again. I think that is what Lean libraries are for.
- sebzim4500 2y agoPossibly but lean libraries currently contain a tiny fraction of widely known mathematical results.