How many theorems in "List of Theorems" of Wikipedia are proven by Metamath?

[Alexander van der Vekens]

Accidentally, I found the "List of Theorems" in Wikipedia (https://en.wikipedia.org/wiki/List_of_theorems). This list contains more than 1000 theorems (I think the exact number is 1139), and I wonder how many of them are proven formally with Metamath. The number of theorems goes far beyond the number of the  "100 theorem list" (http://www.cs.ru.nl/%7Efreek/100/, http://us.metamath.org/mm_100.html), although there are some theorems in the "100 theorem list" which are not contained in Wikipedia's list (e.g. the Friendship theorem and Cramer's rule ;-)).

The corresponding German page ("Liste mathematischer Sätze": https://de.wikipedia.org/wiki/Liste_mathematischer_S%C3%A4tze) lists "only" 823 theorems, but they are different from the "List of Theorems" (e.g. the Friendship theorem and Cramer's rule are mentioned there...).

Does anybody wants to volunteer to check which of these theorems are proven with Metamath (set.mm) and to create a list mapping the entries from Wikipedia to the labels in set.mm? This list could be published on the metamath site.

In addition to filling the (small) gap of unproven theorems of the "100 theorem list", I think it could be a challenge to prove currently unproven theorems of this Wikipedia list.

[Thierry Arnoux]

It's probably not a one-shot exercise.

You could create the page with the list, with question marks for all
theorems (or an entry "don't know" in a column "proven in set.mm"), then
anyone can cooperatively update the file to fill in any missing entry
with the correct reference, or "not in set.mm", with maybe some hints
about what is missing to prove them.

_
Thierry

[vvs]

On Thursday, June 27, 2019 at 3:38:23 PM UTC+3, Alexander van der Vekens wrote:

In addition to filling the (small) gap of unproven theorems of the "100 theorem list", I think it could be a challenge to prove currently unproven theorems of this Wikipedia list.

Probably the most straightforward way to complete such a task would be to convert Metamath into interactive courseware. I've accidentally found similar applications for online courses in several universities. Looks like this is a promising trend. Using efforts of many students for doing distributed formalization might be a powerful instrument, but turning it into addictive internet game should attract even more people. Right now existing applications look very isolated from the rest of Metamath activities and their UI is mostly outdated.