Karl Palmskog (Jan 02 2021 at 17:02): Karl Palmskog (Jan 02 2021 at 17:02):Interesting that Lean formalized math libraries are considered among "2020's Biggest Breakthroughs in Math/CS": https://youtu.be/HL7DEkXV_60?t=296
Karl Palmskog (Jan 02 2021 at 19:55):I guess we have to work harder this year on those jumbled, unplanned cities if we want to make the cut :working_on_it:
Michael Soegtrop (Jan 03 2021 at 09:36):I still think one should make solid statistics on how large Coq is vs. Lean. It is not reasonable to compare say a country with a single drawing board city. As mentioned before I would think that MathComp is as large and as well ordered as the Lean math library. Sure there is also a Wild West part in the Coq world, but I think it is an important part of it.
Have a look at this : Coq at OpenHub or another one- Lean is not even there. I guess the large peaks in the "lines per month" statistic is when largish projects have been added. And btw.: the % are relative to all projects registered at OpenHub in all languages. The Coq % is so large that I put it on my to do to make my own statistics.
Btw.: it might make sense to have a look if important Coq projects are registered with OpenHub - industrial users might look at this.
Karl Palmskog (Jan 03 2021 at 15:51):Interesting links, thanks. Indeed a lot seems to boil down to marketing. Compare also Isabelle's AFP, that has around 3 million LOC. From earlier estimates, this is about the size of Coq's CI, yet this was recently claimed by researchers to be the "largest repository of mechanised proofs". I think it may be time to document and perform some definitive ecosystem measurements, so it becomes less subjective.
Last updated: Dec 01 2023 at 04:01 UTC