> Mathematical ideas, even simple ideas, are often hard to transplant from mind to mind.... Our understanding frequently deteriorates as well... The experts in a subject retire and die, or simply move on to other subjects and forget.... In short, mathematics only exists in a living community of mathematicians that spreads understanding and breaths life into ideas both old and new.

One of the great things about software is that you don't need a living community that holds every bit of every code base in their head. You can rely on abstraction boundaries, and then jump down rabbit holes only if and when necessary.

I really wonder how the work of Mathematics will change once computer-encoded proofs become mainstream. I have to imagine that will happen within the next generation or two -- as soon as the automation becomes more helpful than the hindrance of formality.

https://github.com/leanprover-community/mathlib

https://1lab.dev/

You can watch the next generation, or participate, right now.