feat: allow statements of theorems in 1000.yaml (#577)

And display these on the generated webpage as well.

I don't expect the list of theorems with just a statement to grow large,
but for some results, this could be useful.
Accompanies leanprover-community/mathlib4#20637;
it's better to merge this PR first.

make_site.py

@@ -185,7 +185,9 @@ class HundredTheorem:
     number: str
     # a human-readable title
     title: str
-    # if a theorem is formalised in mathlib, the archive or counterexamples,
+    # If a theorem is merely *stated* in mathlib, the name of the declaration
+    statement: Optional[str] = None
+    # if a theorem is formalized in mathlib, the archive or counterexamples,
     # the name of the corresponding declaration (optional)
     decl: Optional[str] = None
     # like |decl|, but a list of declarations (if one theorem is split into multiple declarations) (optional)
@@ -202,7 +204,7 @@ class HundredTheorem:
 # See https://github.com/1000-plus/1000-plus.github.io/blob/main/README.md#file-format
 # for the specification. Compared to the README,
 # - this |wikidata| field concatenates the upstream fielcs |wikidata| and |id_suffix|
-# - we omit some fields (for now), e.g. the msc classification, and only care about Lean formalisations
+# - we omit some fields (for now), e.g. the msc classification, and only care about Lean formalizations
 @dataclass
 class ThousandPlusTheorem:
     """
@@ -216,7 +218,9 @@ class ThousandPlusTheorem:
     wikidata: str
     # a human-readable title
     title: str
-    # if a theorem is formalised in mathlib, the archive or counterexamples,
+    # If a theorem is merely *stated* in mathlib, the name of the declaration
+    statement: Optional[str] = None
+    # if a theorem is formalized in mathlib, the archive or counterexamples,
     # the name of the corresponding declaration (optional)
     decl: Optional[str] = None
     # like |decl|, but a list of declarations (if one theorem is split into multiple declarations) (optional)
@@ -230,6 +234,7 @@ class ThousandPlusTheorem:
     # any additional notes or comments
     comment: Optional[str] = None
 
+
 @dataclass
 class TheoremForWebpage:
     """
@@ -247,8 +252,10 @@ class TheoremForWebpage:
     """
     id: str
     title: str
-    # A boolean tagging theorems that have been formalized
-    formalized: bool
+    # Whether just the theorem statement has been formalized
+    statement_formalized: bool
+    # Whether this theorem's proof has been formalized
+    proof_formalized: bool
     # The HTML source code for the generated documentation entries
     # for the declaration associated to this theorem.
     doc_decls: Optional[List[DocDecl]]
@@ -339,15 +346,21 @@ def download_N_theorems(kind: NTheorems) -> dict:
     if DOWNLOAD:
         download(f'https://leanprover-community.github.io/mathlib4_docs/{fname}', DATA/fname)
         with (DATA/fname).open('r', encoding='utf-8') as h_file:
-            n_theorems = [Type(thm,**content) for (thm,content) in yaml.safe_load(h_file).items()]
+            n_theorems = [Type(thm, **content) for (thm, content) in yaml.safe_load(h_file).items()]
             theorems = []
             for h in n_theorems:
                 assert not (h.decl and h.decls)
+                assert not (h.statement and (h.decl or h.decls))
+                statement_formalized = False
                 if kind == NTheorems.Hundred:
                     (id, links, thms, note) = (h.number, h.links, '100 theorems', h.note)
                 else:
                     (id, links, thms, note) = (h.wikidata, {'url': h.url} if h.url else {}, '1000+ theorems', h.comment)
-                decls = h.decls or ([h.decl] if h.decl else [])
+                    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
+                decls = h.decls or ([h.decl] if h.decl else []) or ([h.statement] if h.statement else [])
                 doc_decls = []
                 if decls:
                     for decl in decls:
@@ -364,9 +377,8 @@ def download_N_theorems(kind: NTheorems) -> dict:
                             # note: the `header-data.json` data file uses doc-relative links
                             docs_link='/mathlib4_docs/' + decl_info.info.docLink,
                             src_link=decl_info.info.sourceLink))
-                # A theorem counts as formalized if the author field or `doc_decls` is non-empty.
-                formalized = bool(h.author) or (len(doc_decls) > 0)
-                theorems.append(TheoremForWebpage(id, h.title, formalized, doc_decls, links, h.author, h.date, note))
+
+                theorems.append(TheoremForWebpage(id, h.title, statement_formalized, proof_formalized, doc_decls, links, h.author, h.date, note))
         pkl_dump(name, theorems)
     else:
         theorems = pkl_load(name, dict())

templates/100-missing.html

@@ -4,10 +4,25 @@
 {% markdown %}
 # Missing theorems from [Freek Wiedijk's](https://www.cs.ru.nl/~freek/) [list of 100 theorems](https://www.cs.ru.nl/~freek/100/)
 These theorems are not yet formalized in Lean.
-Currently there are {{hundred_theorems|rejectattr('formalized')|list|length}} of them.
+Currently there are {{hundred_theorems|rejectattr('proof_formalized')|list|length}} of them.
+Among these, {{hundred_theorems|rejectattr('proof_formalized')|selectattr('statement_formalized')|list|length}} have their statement formalized.
 <a href="100.html">Here</a> is the list of the formalized theorems.
-{% for theorem in hundred_theorems|rejectattr('formalized') %}
+{% for theorem in hundred_theorems|rejectattr('proof_formalized') %}
 * {{ theorem.id }}: {{ theorem.title }}
 {% endfor %}
+
+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.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>
+    <p><a href="{{ doc.docs_link }}">docs</a>, <a href="{{ doc.src_link }}">source</a></p>
+    {% endfor %}
+    {% for title, link in (theorem.links|default({}, true)).items() %}<p><a href="{{link}}">{{title}}</a></p>{% endfor %}
+    {% if theorem.note %}<p>{% markdown %}{{ theorem.note }}{% endmarkdown %}</p>{% endif %}
+{% endfor %}
+
 {% endmarkdown %}
 {% endblock %}

templates/100.html

@@ -2,11 +2,13 @@
 {% block title %}100 theorems in Lean{% endblock %}
 {% block content %}
 
-        <h1>100 theorems</h1>
+    <h1>100 theorems</h1>
 
-        <p><a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk</a> maintains <a href="https://www.cs.ru.nl/~freek/100/">a list</a> tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers.
-        Currently {{hundred_theorems|selectattr('formalized')|list|length}} of them are formalized in Lean.
-        We also have a page with the theorems from the list <a href="100-missing.html">not yet in Lean</a>.</p>
+    <p><a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk</a> maintains <a href="https://www.cs.ru.nl/~freek/100/">a list</a> tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers.
+    Currently {{hundred_theorems|selectattr('proof_formalized')|list|length}} of them are formalized in Lean,
+    and {{hundred_theorems|rejectattr('proof_formalized')|selectattr('statement_formalized')|list|length}} additional theorem(s) have just their statement formalized in Lean.
+
+    We also have a page with the theorems from the list <a href="100-missing.html">not yet in Lean</a>.</p>
 
 	<p>
 	To make updates to this list, please <a href="contribute/index.html">make a pull request to mathlib</a>
@@ -16,7 +18,7 @@ <h1>100 theorems</h1>
 	<a href="https://docs.github.com/en/github/managing-files-in-a-repository/editing-files-in-another-users-repository">"Editing files in another user's repository"</a>.
 	</p>
 
-    {% for theorem in hundred_theorems|selectattr('formalized') %}
+    {% 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.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}

templates/1000-missing.html

@@ -3,11 +3,26 @@
 {% block content %}
 {% markdown %}
 # Missing theorems from [Freek Wiedijk's](https://www.cs.ru.nl/~freek/) [1000+ theorems project](https://1000-plus.github.io/)
-These theorems are not yet formalized in Lean (or, these formalisations are not entered in the database yet).
-Currently there are {{thousand_theorems|rejectattr('formalized')|list|length}} of them.
+These theorems are not yet formalized in Lean (or, these formalizations are not entered in the database yet).
+Currently there are {{thousand_theorems|rejectattr('proof_formalized')|list|length}} of them.
+Among these, {{thousand_theorems|rejectattr('proof_formalized')|selectattr('statement_formalized')|list|length}} have their statement formalized.
 <a href="1000.html">Here</a> is the list of the formalized theorems.
-{% for theorem in thousand_theorems|rejectattr('formalized') %}
+{% for theorem in thousand_theorems|rejectattr('proof_formalized') %}
 * {{ theorem.id }}: {{ theorem.title }}
 {% endfor %}
+
+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.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>
+    <p><a href="{{ doc.docs_link }}">docs</a>, <a href="{{ doc.src_link }}">source</a></p>
+    {% endfor %}
+    {% for title, link in (theorem.links|default({}, true)).items() %}<p><a href="{{link}}">{{title}}</a></p>{% endfor %}
+    {% if theorem.note %}<p>{% markdown %}{{ theorem.note }}{% endmarkdown %}</p>{% endif %}
+{% endfor %}
+
 {% endmarkdown %}
 {% endblock %}

templates/1000.html

@@ -2,11 +2,12 @@
 {% block title %}1000+ theorems in Lean{% endblock %}
 {% block content %}
 
-        <h1>1000+ theorems</h1>
+    <h1>1000+ theorems</h1>
 
-        <p><a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk</a> started the <a href="https://1000-plus.github.io/">1000+ theorems project</a> tracking progress of theorem provers in formalizing named theorems on wikipedia, as a way of comparing prominent theorem provers.
-        Currently {{thousand_theorems|selectattr('formalized')|list|length}} of them are formalized in Lean.
-        We also have a page with the theorems from the list <a href="1000-missing.html">not yet in Lean</a>.</p>
+    <p><a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk</a> started the <a href="https://1000-plus.github.io/">1000+ theorems project</a> tracking progress of theorem provers in formalizing named theorems on wikipedia, as a way of comparing prominent theorem provers.
+    Currently {{thousand_theorems|selectattr('proof_formalized')|list|length}} of them are formalized in Lean,
+    and {{thousand_theorems|selectattr('statement_formalized')|list|length}} additional theorem(s) have just their statement formalized in Lean.
+    We also have a page with the theorems from the list <a href="1000-missing.html">not yet in Lean</a>.</p>
 
 	<p>
 	To make updates to this list, please <a href="contribute/index.html">make a pull request to mathlib</a>
@@ -16,7 +17,20 @@ <h1>1000+ theorems</h1>
 	<a href="https://docs.github.com/en/github/managing-files-in-a-repository/editing-files-in-another-users-repository">"Editing files in another user's repository"</a>.
 	</p>
 
-    {% for theorem in thousand_theorems|selectattr('formalized') %}
+    {% 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.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>
+        <p><a href="{{ doc.docs_link }}">docs</a>, <a href="{{ doc.src_link }}">source</a></p>
+        {% endfor %}
+        {% for title, link in (theorem.links|default({}, true)).items() %}<p><a href="{{link}}">{{title}}</a></p>{% endfor %}
+        {% if theorem.note %}<p>{% markdown %}{{ theorem.note }}{% endmarkdown %}</p>{% endif %}
+    {% endfor %}
+
+    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.statement %}<p><code>{{ theorem.statement }}</code></p>{% endif %}