Re:Building the Mathematical Library of the Future
by yaseer on Thursday November 12, 2020 @05:59AM
(#25068586)
I agree, and discussed this a little.
There is one key difference with the theorem provers- many of them share this lofty goal of building a library, akin to a 'library of Alexandria' (The article discusses this vision, and the research project I linked to at Cambridge is called 'Alexandria').
It's a grand vision - to formalise all mathematical knowledge in a library.
This vision doesn't exist in the world of regular software.
Nobody to my mind has claimed they're building a library of Alexandria. You could make the claim for npm, but I might shed a tear if you did that.
There is one key difference with the theorem provers- many of them share this lofty goal of building a library, akin to a 'library of Alexandria' (The article discusses this vision, and the research project I linked to at Cambridge is called 'Alexandria').
It's a grand vision - to formalise all mathematical knowledge in a library.
This vision doesn't exist in the world of regular software.
Nobody to my mind has claimed they're building a library of Alexandria. You could make the claim for npm, but I might shed a tear if you did that.