Wikipedia

Stream: new members

[Marcus Zibrowius]

The wikipedia entry on the QED manifesto states:

"[T]he Mizar library has successfully formalized a large portion of undergraduate mathematics. As of 2007 it is the largest such library."

Obviously, this is outdated. What should the page say today? And is there a meaningful quantitative way to compare the Mizar library with mathlib?

[Anne Baanen]

We maintain a list of undergraduate mathematics formalized in Lean, based on the French curriculum. So my first suggestion would be to compare the percentage of completion of that list to that of Mizar.

[Anne Baanen]

Another quick and dirty comparison would be the progress on the top 100 theorems. Apparently Lean is now ahead of Mizar by 1 whole theorem!

[Alex J. Best]

I think it's very difficult to make such comparisons, especially in this somewhat rapidly changing area, most obvious metrics have flaws. The aim of a reference work like Wikipedia should probably instead stick to mentioning some big projects in the area, when the absolute "largest" is hard to pin down with a reasonable measure of size.

[Marcus Zibrowius]

Thanks for the links! I just thought it would be appropriate to mention mathlib on that page. And if it was possible to make a vague quantitative comparison, I would also include it there. But I can't find as a good an overview over what parts of the curriculum are actually covered by the Mizar library. So for now I've just made the most minimal edit to the Wikipedia page:

The Mizar Mathematical Library formalizes a large portion of undergraduate mathematics, and was considered the largest such library in 2007.[4] Similar projects include the Metamath proof database and the mathlib library written in Lean.[5]