3 ms·

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 explo

by ipnon 2y ago

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.

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 ago
  Possibly but lean libraries currently contain a tiny fraction of widely known mathematical results.