The Effort to Build the Mathematical Library of the Future.
A community of mathematicians is using software called Lean to build a new digital repository.
By Kevin Hartnett
There are huge, important areas of math that have never been fully written down. They’re stored in the minds of a small circle of people who learned their subfield of math from people who learned it from the person who invented it—which is to say, it exists nearly as folklore.
https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/