Missing module docstrings + type_of% theorem links

FormalConjectures/Wikipedia/BrocardProblem.lean

@@ -15,3 +15,26 @@ limitations under the License.
 -/
 
 import FormalConjectures.ErdosProblems.«398»
+
+/-!
+# Brocard's Problem
+
+Brocard's problem asks whether the only solutions to $n! + 1 = m^2$ are
+$n = 4, 5, 7$.
+
+*Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Brocard%27s_problem)
+
+This file points to the canonical formalization in `FormalConjectures.ErdosProblems.«398»`.
+-/
+
+namespace BrocardProblem
+
+/--
+This Wikipedia entry points to the canonical formalization of Brocard's problem
+in `FormalConjectures.ErdosProblems.«398»`.
+-/
+@[category research open, AMS 11]
+theorem brocard_problem : type_of% @Erdos398.erdos_398 := by
+  sorry
+
+end BrocardProblem

FormalConjectures/Wikipedia/HadwigerNelson.lean

@@ -17,7 +17,25 @@ limitations under the License.
 import FormalConjectures.ErdosProblems.«508»
 
 /-!
-# The Hadwiger–Nelson problem
+# The Hadwiger-Nelson Problem
+
+The Hadwiger-Nelson problem asks for the minimum number of colors required to
+color the plane such that no two points at unit distance from each other have
+the same color.
 
 *Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Hadwiger%E2%80%93Nelson_problem)
+
+This file points to the canonical formalization in `FormalConjectures.ErdosProblems.«508»`.
+-/
+
+namespace HadwigerNelson
+
+/--
+This Wikipedia entry points to the canonical formalization of the
+Hadwiger-Nelson problem in `FormalConjectures.ErdosProblems.«508»`.
 -/
+@[category research open, AMS 52]
+theorem hadwiger_nelson_problem : type_of% @Erdos508.HadwigerNelsonProblem := by
+  sorry
+
+end HadwigerNelson

FormalConjectures/Wikipedia/HappyEndingProblem.lean

@@ -16,3 +16,27 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 import FormalConjectures.ErdosProblems.«107»
+
+/-!
+# Happy Ending Problem
+
+The happy ending problem asks whether $f(n) = 2^{n-2} + 1$, where $f(n)$ is the
+smallest number such that any $f(n)$ points in general position in the plane
+contain $n$ that form a convex polygon.
+
+*Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Happy_ending_problem)
+
+This file points to the canonical formalization in `FormalConjectures.ErdosProblems.«107»`.
+-/
+
+namespace HappyEndingProblem
+
+/--
+This Wikipedia entry points to the canonical formalization of the happy ending
+problem in `FormalConjectures.ErdosProblems.«107»`.
+-/
+@[category research open, AMS 52]
+theorem happy_ending_problem : type_of% @Erdos107.erdos_107 := by
+  sorry
+
+end HappyEndingProblem

FormalConjectures/Wikipedia/MinimalOverlapProblem.lean

@@ -15,3 +15,28 @@ limitations under the License.
 -/
 
 import FormalConjectures.ErdosProblems.«36»
+
+/-!
+# Minimum Overlap Problem
+
+The minimum overlap problem asks for the limit of the minimum, over all
+splittings of $\{1, \ldots, 2n\}$ into two sets $A$ and $B$ of equal size, of
+the maximum number of representations of any integer $k$ as $a - b$ with
+$a \in A$, $b \in B$, divided by $n$.
+
+*Reference:* [Wikipedia](https://en.wikipedia.org/wiki/Minimum_overlap_problem)
+
+This file points to the canonical formalization in `FormalConjectures.ErdosProblems.«36»`.
+-/
+
+namespace MinimalOverlapProblem
+
+/--
+This Wikipedia entry points to the canonical formalization of the minimum overlap
+problem in `FormalConjectures.ErdosProblems.«36»`.
+-/
+@[category research open, AMS 5 11]
+theorem minimum_overlap_problem : type_of% @Erdos36.erdos_36 := by
+  sorry
+
+end MinimalOverlapProblem

FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean

@@ -16,6 +16,13 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 1
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
 namespace WrittenOnTheWallII.GraphConjecture1
 
 open SimpleGraph

FormalConjectures/WrittenOnTheWallII/GraphConjecture19.lean

@@ -16,6 +16,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 19
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 open Classical
 
 namespace WrittenOnTheWallII.GraphConjecture19

FormalConjectures/WrittenOnTheWallII/GraphConjecture2.lean

@@ -17,6 +17,13 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 2
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
 namespace WrittenOnTheWallII.GraphConjecture2
 
 open Classical SimpleGraph

FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean

@@ -16,6 +16,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 3
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 universe u
 
 namespace WrittenOnTheWallII.GraphConjecture3

FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean

@@ -17,6 +17,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 34
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 open Finset
 open scoped Classical
 

FormalConjectures/WrittenOnTheWallII/GraphConjecture4.lean

@@ -16,6 +16,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 4
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 namespace WrittenOnTheWallII.GraphConjecture4
 
 open SimpleGraph

FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean

@@ -16,6 +16,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 40
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 namespace WrittenOnTheWallII.GraphConjecture40
 
 open SimpleGraph

FormalConjectures/WrittenOnTheWallII/GraphConjecture5.lean

@@ -16,6 +16,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 5
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 namespace WrittenOnTheWallII.GraphConjecture5
 
 open SimpleGraph

FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean

@@ -16,6 +16,14 @@ limitations under the License.
 
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 58
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 namespace WrittenOnTheWallII.GraphConjecture58
 
 open SimpleGraph

FormalConjectures/WrittenOnTheWallII/GraphConjecture6.lean

@@ -15,6 +15,14 @@ limitations under the License.
 -/
 import FormalConjectures.Util.ProblemImports
 
+/-!
+# Written on the Wall II - Conjecture 6
+
+*Reference:*
+[E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc](http://cms.dt.uh.edu/faculty/delavinae/research/wowII/)
+-/
+
+
 open SimpleGraph
 
 namespace WrittenOnTheWallII.GraphConjecture6