deploy site from 5cadbea

leanprover-community · Jan 20, 2025 · aff5ae9 · aff5ae9
1 parent bfdf9fa
commit aff5ae9
Show file tree

Hide file tree

Showing 8 changed files with 724 additions and 571 deletions.
diff --git a/100-missing.html b/100-missing.html
@@ -112,7 +112,6 @@ <h1 id="missing-theorems-from-freek-wiedijks-list-of-100-theorems" class="markdo
 <p>92: Pick’s Theorem</p>
 </li>
 </ul>
-<p>The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.</p>
 
   </main>
 

diff --git a/100.html b/100.html
diff --git a/1000-missing.html b/1000-missing.html
@@ -50,8 +50,8 @@
 
 <h1 id="missing-theorems-from-freek-wiedijks-1000-theorems-project" class="markdown-heading">Missing theorems from <a href="https://www.cs.ru.nl/~freek/">Freek Wiedijk's</a> <a href="https://1000-plus.github.io/">1000+ theorems project</a> <a class="hover-link" href="#missing-theorems-from-freek-wiedijks-1000-theorems-project">#</a></h1>
 <p>These theorems are not yet formalized in Lean (or, these formalizations are not entered in the database yet).
-Currently there are 1047 of them.
-Among these, 0 have their statement formalized.
+Currently there are 1041 of them.
+Among these, 2 have their statement formalized.
 <a href="1000.html">Here</a> is the list of the formalized theorems.</p>
 <ul>
 <li>
@@ -82,9 +82,6 @@ <h1 id="missing-theorems-from-freek-wiedijks-1000-theorems-project" class="markd
 <p>Q164262: Lebesgue covering dimension</p>
 </li>
 <li>
-<p>Q172298: Lasker–Noether theorem</p>
-</li>
-<li>
 <p>Q174955: Mihăilescu's theorem</p>
 </li>
 <li>
@@ -94,12 +91,6 @@ <h1 id="missing-theorems-from-freek-wiedijks-1000-theorems-project" class="markd
 <p>Q179692: Independence of the axiom of choice</p>
 </li>
 <li>
-<p>Q180345X: Integral root theorem</p>
-</li>
-<li>
-<p>Q180345: Rational root theorem</p>
-</li>
-<li>
 <p>Q184410: Four color theorem</p>
 </li>
 <li>
@@ -181,12 +172,6 @@ <h1 id="missing-theorems-from-freek-wiedijks-1000-theorems-project" class="markd
 <p>Q256303: Lax–Richtmyer theorem</p>
 </li>
 <li>
-<p>Q257387: Vitali theorem</p>
-</li>
-<li>
-<p>Q258374: Carathéodory's theorem</p>
-</li>
-<li>
 <p>Q260928: Jordan curve theorem</p>
 </li>
 <li>
@@ -283,9 +268,6 @@ <h1 id="missing-theorems-from-freek-wiedijks-1000-theorems-project" class="markd
 <p>Q401905: Skorokhod's representation theorem</p>
 </li>
 <li>
-<p>Q422187: Myhill–Nerode theorem</p>
-</li>
-<li>
 <p>Q425432: Laurent expansion theorem</p>
 </li>
 <li>
@@ -3196,7 +3178,6 @@ <h1 id="missing-theorems-from-freek-wiedijks-1000-theorems-project" class="markd
 <p>Q112740521: Netto's theorem</p>
 </li>
 </ul>
-<p>The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.</p>
 
   </main>
 

diff --git a/1000.html b/1000.html
diff --git a/mathlib-overview.html b/mathlib-overview.html
@@ -982,7 +982,7 @@ <h4 id="probability-theory" class="markdown-heading">Probability Theory<a class=
 
 		<a href="/mathlib4_docs/./Mathlib/Probability/Integration.html#ProbabilityTheory.IndepFun.integral_mul_of_integrable">mean of product of independent random variables</a>, 
 
-		<a href="/mathlib4_docs/./Mathlib/Probability/Moments.html#ProbabilityTheory.moment">moment of a random variable</a>, 
+		<a href="/mathlib4_docs/./Mathlib/Probability/Moments/Basic.html#ProbabilityTheory.moment">moment of a random variable</a>, 
 
 		<a href="/mathlib4_docs/./Mathlib/Probability/ProbabilityMassFunction/Constructions.html#PMF.bernoulli">Bernoulli law</a>.
 
@@ -1148,7 +1148,7 @@ <h4 id="dynamics" class="markdown-heading">Dynamics<a class="hover-link" href="#
 
 		<a href="/mathlib4_docs/./Mathlib/Dynamics/FixedPoints/Basic.html#Function.fixedPoints">fixed points</a>, 
 
-		<a href="/mathlib4_docs/./Mathlib/Dynamics/PeriodicPts.html#Function.periodicPts">periodic points</a>.
+		<a href="/mathlib4_docs/./Mathlib/Dynamics/PeriodicPts/Defs.html#Function.periodicPts">periodic points</a>.
 
 
 	  </p>

diff --git a/mathlib_stats.html b/mathlib_stats.html
@@ -60,9 +60,9 @@ <h2>Counts</h2>
             <th>Contributors</th>
         </tr>
         <tr>
-            <td>94556</td>
-            <td>181187</td>
-            <td>384</td>
+            <td>94681</td>
+            <td>181569</td>
+            <td>385</td>
         </tr>
     </table>
 

diff --git a/meet.html b/meet.html
diff --git a/undergrad.html b/undergrad.html
@@ -1062,7 +1062,7 @@ <h4>Probability Theory</h4>
 
           <a href="/mathlib4_docs/./Mathlib/Probability/Variance.html#ProbabilityTheory.variance">variance of a real-valued random variable</a>, 
 
-          <a href="/mathlib4_docs/./Mathlib/Probability/Moments.html#ProbabilityTheory.moment">moments</a>, 
+          <a href="/mathlib4_docs/./Mathlib/Probability/Moments/Basic.html#ProbabilityTheory.moment">moments</a>, 
 
           <a href="/mathlib4_docs/./Mathlib/Probability/ProbabilityMassFunction/Constructions.html#PMF.bernoulli">Bernoulli law</a>.
-Original file line number
+Diff line change
@@ Expand Up @@
     <p>92: Pick’s Theorem</p>
     </li>
     </ul>
-    <p>The following theorem(s) have just their statement formalized. Contributions to their proofs are welcome.</p>
       </main>
@@ Expand Down @@