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”.

Now 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.

> 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.

Possibly but lean libraries currently contain a tiny fraction of widely known mathematical results.