Stream: Miscellaneous

Topic: Math/CS 2020 breakthroughs


view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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: Aug 19 2022 at 19:03 UTC