3 ms·

I guess Coq/Lean standard libraries fit this definition.

• cloogshicer 6y ago
  Exactly, I got this idea from a talk about Lean: https://www.youtube.com/watch?v=Dp-mQ3HxgDE https://www.youtube.com/watch?v=Dp-mQ3HxgDE
  • seanwilson 6y ago
    You should look at this like software development. New programming languages come out that try to solve the problems of all the previous languages and unify everyone to code and be productive in the same ecosystem...until another language comes out etc. It's very hard to get everyone to agree how code plus mathematics should be written. There's a lot of fragmentation and ongoing attempts to unify.