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 Wikidedia'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 challange to prove currently unproven
theorems of this Wikipedia list.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/fb9b2c22-313c-4515-934a-b180d0655a11%40googlegroups.com.
