Rebrand from "1000plus" to "Wikipedia's list of theorems"

references.bib

@@ -1,6 +1,7 @@
 @online{1000+theorems,
   title  = {1000+ theorems},
-  author = {Freek Wiedijk},
+  author = {1000plus},
+  citeas = {1000+},
   url    = {https://1000-plus.github.io/}
 }
 

src/literature.lagda.md

@@ -10,11 +10,11 @@
 module literature where
 
 open import literature.100-theorems public
-open import literature.1000plus-theorems public
 open import literature.idempotents-in-intensional-type-theory public
 open import literature.introduction-to-homotopy-type-theory public
 open import literature.oeis public
 open import literature.sequential-colimits-in-homotopy-type-theory public
+open import literature.wikipedia-list-of-theorems public
 ```
 
 ## References

src/literature/100-theorems.lagda.md

@@ -1,4 +1,4 @@
-# Freek Wiedijk's 100 Theorems
+# Wiedijk's 100 Theorems
 
 This file records formalized results from
 [Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/)'s
@@ -145,8 +145,7 @@ open import real-numbers.metric-space-of-real-numbers using
 
 ## See also
 
-- The spiritual successor to _Formalizing 100 Theorems_ is
-  [_1000+ theorems_](literature.1000plus-theorems.md), also due to Freek Wiedijk
+- The spiritual successor to _Formalizing 100 Theorems_ is _1000+ theorems_
   {{#cite 1000+theorems}}.
 
 ## References

src/literature/1000plus-theorems.lagda.md → src/literature/wikipedia-list-of-theorems.lagda.md

@@ -1,20 +1,20 @@
-# 1000+ theorems
+# Wikipedia's list of theorems
 
-On this page, we record formalized results in the agda-unimath library following
-[Freek Wiedijk](http://www.cs.ru.nl/F.Wiedijk/) and
-[collaborators](https://github.com/1000-plus)'
-[_1000+ theorems_](https://1000-plus.github.io/) project
-{{#cite 1000+theorems}}. This project records the formalization status of
-theorems in mathematics that have their own Wikipedia entry. We welcome any
-contribution to this list!
+On this page, we record formalized results in the agda-unimath library that are
+on
+[Wikipedia's list of theorems](https://en.wikipedia.org/wiki/List_of_theorems)
+or have a Wikidata entry listed as an instance of a
+[theorem](https://www.wikidata.org/wiki/Q65943). Additions to this list are very
+welcome!
 
 ```agda
-module literature.1000plus-theorems where
+module literature.wikipedia-list-of-theorems where
 ```
 
 ## Formalized theorems
 
-The theorems are ordered alphabetically, omitting definite articles ("the").
+The theorems are ordered alphabetically, omitting leading definite articles
+("the").
 
 ### Bézout's lemma {#Q513028}
 
@@ -159,19 +159,11 @@ open import category-theory.yoneda-lemma-precategories using
   ( lemma-yoneda-Precategory)
 ```
 
-## See also
-
-- The spiritual predecessor of _1000+ theorems_ is
-  [_Formalizing 100 Theorems_](literature.100-theorems.md), also due to Freek
-  Wiedijk {{#cite 100theorems}}.
-
-## References
-
-{{#bibliography}}
-
 ## External links
 
 - [List of theorems](https://en.wikipedia.org/wiki/List_of_theorems) on
   Wikipedia
-- [1000+ theorems](https://1000-plus.github.io/)
-- [1000-plus](https://github.com/1000-plus/1000-plus.github.io) on GitHub
+- The [1000plus project](https://github.com/1000-plus)'s
+  [_1000+ theorems_](https://1000-plus.github.io/) records formalized results
+  from Wikipedia's list of theorems in the 6 proof assistants Isabelle, HOL
+  Light, Coq/Rocq, Lean, Metamath, and Mizar.