chore: use 'authors' for the authors field in {Hundred,Thousand}Theor…

…ems (#578)

This matches the `Formalization` type in `make_site.py`, and the mathlib
PR leanprover-community/mathlib4#20875.

make_site.py

@@ -193,7 +193,7 @@ class HundredTheorem:
     # like |decl|, but a list of declarations (if one theorem is split into multiple declarations) (optional)
     decls: Optional[List[str]] = None
     # name(s) of the author(s) of this formalization (optional)
-    author: Optional[str] = None
+    authors: Optional[str] = None
     # Date of the formalization, in the form `YYYY`, `YYYY-MM` or `YYYY-MM-DD` (optional)
     date: Optional[str] = None
     links: Optional[Mapping[str, str]] = None
@@ -226,7 +226,7 @@ class ThousandPlusTheorem:
     # like |decl|, but a list of declarations (if one theorem is split into multiple declarations) (optional)
     decls: Optional[List[str]] = None
     # name(s) of the author(s) of this formalization (optional)
-    author: Optional[str] = None
+    authors: Optional[str] = None
     # Date of the formalization, in the form `YYYY`, `YYYY-MM` or `YYYY-MM-DD` (optional)
     date: Optional[str] = None
     # for external projects, an URL referring to the result
@@ -260,8 +260,8 @@ class TheoremForWebpage:
     # for the declaration associated to this theorem.
     doc_decls: Optional[List[DocDecl]]
     links: Optional[Mapping[str, str]] = None
-    # See above for the meaning of |author|, |date| and |note|.
-    author: Optional[str] = None
+    # See above for the meaning of |authors|, |date| and |note|.
+    authors: Optional[str] = None
     date: Optional[str] = None
     note: Optional[str] = None
 
@@ -358,8 +358,8 @@ def download_N_theorems(kind: NTheorems) -> dict:
                     (id, links, thms, note) = (h.wikidata, {'url': h.url} if h.url else {}, '1000+ theorems', h.comment)
                     if h.statement:
                         statement_formalized = True
-                # A theorem's proof counts as formalized if the author or `decl`(s) field is non-empty.
-                proof_formalized = bool(h.author) or h.decls or h.decl
+                # A theorem's proof counts as formalized if the authors or `decl`(s) field is non-empty.
+                proof_formalized = bool(h.authors) or h.decls or h.decl
                 decls = h.decls or ([h.decl] if h.decl else []) or ([h.statement] if h.statement else [])
                 doc_decls = []
                 if decls:
@@ -378,7 +378,7 @@ def download_N_theorems(kind: NTheorems) -> dict:
                             docs_link='/mathlib4_docs/' + decl_info.info.docLink,
                             src_link=decl_info.info.sourceLink))
 
-                theorems.append(TheoremForWebpage(id, h.title, statement_formalized, proof_formalized, doc_decls, links, h.author, h.date, note))
+                theorems.append(TheoremForWebpage(id, h.title, statement_formalized, proof_formalized, doc_decls, links, h.authors, h.date, note))
         pkl_dump(name, theorems)
     else:
         theorems = pkl_load(name, dict())

templates/100-missing.html

@@ -14,7 +14,7 @@
 The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.
 {% for theorem in thousand_theorems|selectattr('statement_formalized') %}
     <h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
-    {% if theorem.author %}<p>Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}</p>{% endif %}
+    {% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
     {% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
     {% for doc in theorem.doc_decls|default([], true) %}
     <div class="doc-stmt">{{ doc.decl_header_html }}</div>

templates/100.html

@@ -20,7 +20,7 @@ <h1>100 theorems</h1>
 
     {% for theorem in hundred_theorems|selectattr('proof_formalized') %}
         <h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}. {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
-        {% if theorem.author %}<p>Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}</p>{% endif %}
+        {% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
         {% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
         {% for doc in theorem.doc_decls|default([], true) %}
         <div class="doc-stmt">{{ doc.decl_header_html }}</div>

templates/1000-missing.html

@@ -14,7 +14,7 @@
 The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.
 {% for theorem in thousand_theorems|selectattr('statement_formalized') %}
     <h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
-    {% if theorem.author %}<p>Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}</p>{% endif %}
+    {% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
     {% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
     {% for doc in theorem.doc_decls|default([], true) %}
     <div class="doc-stmt">{{ doc.decl_header_html }}</div>

templates/1000.html

@@ -19,7 +19,7 @@ <h1>1000+ theorems</h1>
 
     {% for theorem in thousand_theorems|selectattr('proof_formalized') %}
         <h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
-        {% if theorem.author %}<p>Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}</p>{% endif %}
+        {% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
         {% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
         {% for doc in theorem.doc_decls|default([], true) %}
         <div class="doc-stmt">{{ doc.decl_header_html }}</div>
@@ -32,7 +32,7 @@ <h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ the
     The following theorems have just their statement formalized. Contributions to their proofs are welcome.
     {% for theorem in thousand_theorems|selectattr('statement_formalized') %}
         <h5 class="markdown-heading mt-5" id="{{ theorem.id }}">{{ theorem.id }}: {{ theorem.title }} <a class="hover-link" href="#{{ theorem.id }}">#</a></h5>
-        {% if theorem.author %}<p>Author{% if ' and ' in theorem.author %}s{% endif %}: {{ theorem.author }}</p>{% endif %}
+        {% if theorem.authors %}<p>Author{% if ' and ' in theorem.authors %}s{% endif %}: {{ theorem.authors }}</p>{% endif %}
         {% if theorem.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}
         {% for doc in theorem.doc_decls|default([], true) %}
         <div class="doc-stmt">{{ doc.decl_header_html }}</div>