diff --git a/FormalConjectures/Wikipedia/BrocardProblem.lean b/FormalConjectures/Wikipedia/BrocardProblem.lean index 87033d01d..260757db2 100644 --- a/FormalConjectures/Wikipedia/BrocardProblem.lean +++ b/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 diff --git a/FormalConjectures/Wikipedia/HadwigerNelson.lean b/FormalConjectures/Wikipedia/HadwigerNelson.lean index cb5aa2930..3e22eefc9 100644 --- a/FormalConjectures/Wikipedia/HadwigerNelson.lean +++ b/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 diff --git a/FormalConjectures/Wikipedia/HappyEndingProblem.lean b/FormalConjectures/Wikipedia/HappyEndingProblem.lean index b7814b623..9473a73a7 100644 --- a/FormalConjectures/Wikipedia/HappyEndingProblem.lean +++ b/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 diff --git a/FormalConjectures/Wikipedia/MinimalOverlapProblem.lean b/FormalConjectures/Wikipedia/MinimalOverlapProblem.lean index 6a8d4fcf1..b9b5659dc 100644 --- a/FormalConjectures/Wikipedia/MinimalOverlapProblem.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean index 588ee56ca..2228fd6d6 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture1.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture19.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture19.lean index 43462ee41..d5aa309c7 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture19.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture2.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture2.lean index 921034184..1d2e3de40 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture2.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean index 727c36cb6..e6f280376 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture3.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean index 749078976..f734d3287 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture34.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture4.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture4.lean index e4751c408..0c6e2ce93 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture4.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean index b27a0e46c..0059ea4e3 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture40.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture5.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture5.lean index 539c5688b..ecc15d593 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture5.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean index a1a9cb6c4..60df945ed 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture58.lean +++ b/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 diff --git a/FormalConjectures/WrittenOnTheWallII/GraphConjecture6.lean b/FormalConjectures/WrittenOnTheWallII/GraphConjecture6.lean index a42779980..d9efe6f03 100644 --- a/FormalConjectures/WrittenOnTheWallII/GraphConjecture6.lean +++ b/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