Hacker News new | ask | show | jobs
by hirple 1932 days ago
I guess Coq/Lean standard libraries fit this definition.
1 comments

Exactly, I got this idea from a talk about Lean: https://www.youtube.com/watch?v=Dp-mQ3HxgDE
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.