Merge branch 'main' into milikic/beck-fiala-formal-proof

Author: Lemmy00

FormalConjectures/ErdosProblems/1020.lean

@@ -0,0 +1,80 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1020
+
+*References:*
+- [erdosproblems.com/1020](https://www.erdosproblems.com/1020)
+- [BDE76] Bollobás, B. and Daykin, D. E. and Erdős, P., *Sets of independent edges of a hypergraph*.
+  Quart. J. Math. Oxford Ser. (2) (1976), 25--32.
+- [Er65d] Erdős, P., *A problem on independent {$r$}-tuples*. Ann. Univ. Sci. Budapest. Eötvös Sect.
+  Math. (1965), 93--95.
+- [ErGa59] Erdős, P. and Gallai, T., *On maximal paths and circuits of graphs*. Acta Math. Acad.
+  Sci. Hungar. (1959), 337-356 (unbound insert).
+- [FLM12] Frankl, Peter and Łuczak, Tomasz and Mieczkowska, Katarzyna, *On matchings in
+  hypergraphs*. Electron. J. Combin. (2012), Paper 42, 5.
+- [FRR12] Frankl, Peter and Rödl, Vojtech and Ruciński, Andrzej, *On the maximum number of edges in
+  a triple system not containing a disjoint family of a given size*. Combin. Probab. Comput. (2012),
+  141--148.
+- [Fr17] Frankl, Peter, *Proof of the {E}rdős matching conjecture in a new range*. Israel J. Math.
+  (2017), 421--430.
+- [Fr87] Frankl, Peter, *The shifting technique in extremal set theory*. (1987), 81--110.
+- [HLS12] Huang, Hao and Loh, Po-Shen and Sudakov, Benny, *The size of a hypergraph and its matching
+  number*. Combin. Probab. Comput. (2012), 442--450.
+- [Kl68] Kleitman, Daniel J., *Maximal number of subsets of a finite set no {$k$} of which are
+  pairwise disjoint*. J. Combinatorial Theory (1968), 157--163.
+- [KoKu23] Kolupaev, Dmitriy and Kupavskii, Andrey, *Erdős matching conjecture for almost perfect
+  matchings*. Discrete Math. (2023), Paper No. 113304, 9.
+- [LuMi14] Łuczak, Tomasz and Mieczkowska, Katarzyna, *On {E}rdős' extremal problem on matchings in
+  hypergraphs*. J. Combin. Theory Ser. A (2014), 178--194.
+-/
+
+namespace Erdos1020
+
+/-- The maximum number of edges in an `r`-uniform hypergraph on `n` vertices containing no
+matching of size `k` (i.e. no `k` pairwise vertex-disjoint edges). -/
+noncomputable def f (n r k : ℕ) : ℕ :=
+  sSup {m : ℕ | ∃ H : Hypergraph (Fin n),
+    H.vertexSet = Set.univ ∧
+    (∀ e ∈ H.edgeSet, e.ncard = r) ∧
+    (¬ ∃ M ⊆ H.edgeSet, M.ncard = k ∧ M.PairwiseDisjoint id) ∧
+    H.edgeSet.ncard = m}
+
+/--
+Let $f(n;r,k)$ be the maximal number of edges in an $r$-uniform hypergraph which contains no set of $k$ many independent edges.
+
+For all $r\geq 3$, $$f(n;r,k)=\max\left(\binom{rk-1}{r}, \binom{n}{r}-\binom{n-k+1}{r}\right).$$
+
+Note: the source states the formula with no range on `n` or `k`, but some restriction
+is needed: e.g. for `r = 3`, `k = 2`, `n = 4` no two disjoint triples fit in `4`
+vertices, so the left-hand side is `4.choose 3 = 4` while the right-hand side is
+`5.choose 3 = 10`. We require `k ≥ 1` and `n ≥ r*k - 1`: this is the smallest `n`
+accommodating the construction counted by the first term (all `r`-subsets of a fixed
+`(r*k - 1)`-set), and at `n = r*k - 1` the equality holds trivially, since the complete
+`r`-uniform hypergraph has no `k`-matching. The source's commentary likewise calls the
+case `n < k*r` trivial.
+-/
+@[category research open, AMS 5]
+theorem erdos_1020 (r : ℕ) (hr : 3 ≤ r) (n k : ℕ) (hk : 0 < k)
+    (hrk : r * k - 1 ≤ n) :
+    f n r k = max ((r * k - 1).choose r)
+      (n.choose r - (n - k + 1).choose r) := by
+  sorry
+
+end Erdos1020

FormalConjectures/ErdosProblems/104.lean

@@ -0,0 +1,62 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 104
+
+*References:*
+- [erdosproblems.com/104](https://www.erdosproblems.com/104)
+- [El84] Elekes, G., *{$n$} points in the plane can determine $n^{3/2}$ unit circles*. Combinatorica
+  (1984), 131.
+- [Er75h] Erdős, P., *Some problems on elementary geometry*. Austral. Math. Soc. Gaz. (1975), 2-3.
+- [Er81d] Erdős, P., *Some applications of graph theory and combinatorial methods to number theory
+  and geometry*. Algebraic methods in graph theory, Vol. I, II (Szeged, 1978) (1981), 137-148.
+- [Er92e] Erdős, Pál, *Some Unsolved problems in Geometry, Number Theory and Combinatorics*. Eureka
+  (1992), 44-48.
+- [HaMe86] Harborth, Heiko and Mengersen, Ingrid, *Point sets with many unit circles*. Discrete
+  Math. (1986), 193--197.
+-/
+
+open Filter
+open scoped EuclideanGeometry
+
+namespace Erdos104
+
+open EuclideanGeometry
+
+/-- The number of distinct unit circles containing at least three points of `P`. -/
+noncomputable def unitCircleCount (P : Finset ℝ²) : ℕ :=
+  Set.ncard {s : Sphere ℝ² | s.radius = 1 ∧ 3 ≤ {p ∈ (P : Set ℝ²) | p ∈ s}.ncard}
+
+/-- The set of unit-circle counts attained by configurations of `n` points in the plane. -/
+noncomputable def possibleUnitCircleCounts (n : ℕ) : Set ℕ :=
+  {k | ∃ P : Finset ℝ², P.card = n ∧ unitCircleCount P = k}
+
+/-- The maximum number of qualifying unit circles attained by a configuration of `n` points. -/
+noncomputable def maxUnitCircleCount (n : ℕ) : ℕ :=
+  sSup (possibleUnitCircleCounts n)
+
+/--
+Given $n$ points in $\mathbb{R}^2$ the number of distinct unit circles containing at least three points is $o(n^2)$.
+-/
+@[category research open, AMS 52]
+theorem erdos_104 :
+    (fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2) := by
+  sorry
+
+end Erdos104

FormalConjectures/ErdosProblems/1083.lean

@@ -0,0 +1,49 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1083
+
+*References:*
+- [erdosproblems.com/1083](https://www.erdosproblems.com/1083)
+- [APST04] Aronov, Boris and Pach, János and Sharir, Micha and Tardos, Gábor, *Distinct distances in
+  three and higher dimensions*. Combin. Probab. Comput. (2004), 283--293.
+- [CEGSW90] Clarkson, Kenneth L. and Edelsbrunner, Herbert and Guibas, Leonidas J. and Sharir, Micha
+  and Welzl, Emo, *Combinatorial complexity bounds for arrangements of curves and spheres*. Discrete
+  Comput. Geom. (1990), 99--160.
+- [Er46b] Erdős, P., *On sets of distances of {$n$} points*. Amer. Math. Monthly (1946), 248--250.
+- [SoVu08] Solymosi, József and Vu, Van H., *Near optimal bounds for the {E}rdős distinct distances
+  problem in high dimensions*. Combinatorica (2008), 113--125.
+-/
+
+open Filter
+open scoped EuclideanGeometry
+
+namespace Erdos1083
+
+/--
+Let $d\geq 3$, and let $f_d(n)$ be the minimal $m$ such that every set of $n$ points in $\mathbb{R}^d$ determines at least $m$ distinct distances. Estimate $f_d(n)$ - in particular, is it true that $$f_d(n)=n^{\frac{2}{d}-o(1)}?$$
+-/
+@[category research open, AMS 52]
+theorem erdos_1083 : answer(sorry) ↔
+    ∀ d : ℕ, 3 ≤ d → ∃ o : ℕ → ℝ, o =o[atTop] (1 : ℕ → ℝ) ∧
+      ∀ᶠ n : ℕ in atTop,
+        (minimalDistinctDistances (ℝ^d) n : ℝ) = (n : ℝ) ^ ((2 : ℝ) / (d : ℝ) - o n) := by
+  sorry
+
+end Erdos1083

FormalConjectures/ErdosProblems/1159.lean

@@ -0,0 +1,47 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1159
+
+*References:*
+- [erdosproblems.com/1159](https://www.erdosproblems.com/1159)
+- [ESS83] Erdős, P. and Silverman, R. and Stein, A., *Intersection properties of families containing
+  sets of nearly the same size*. Ars Combin. (1983), 247--259.
+- [Er81] Erdős, P., *On the combinatorial problems which I would most like to see solved*.
+  Combinatorica (1981), 25-42.
+-/
+
+open Configuration
+
+namespace Erdos1159
+
+/--
+Determine whether there exists a constant $C>1$ such that the following holds.
+
+Let $P$ be a finite [projective plane](https://en.wikipedia.org/wiki/Projective_plane). Must there exist a set of points $S$ such that $1\leq \lvert S\cap \ell\rvert \leq C$ for all lines $\ell$?
+-/
+@[category research open, AMS 5 51]
+theorem erdos_1159 : answer(sorry) ↔
+    ∃ C : ℕ, 1 < C ∧
+      ∀ (P L : Type) (_ : Membership P L) (_ : Fintype P) (_ : Fintype L),
+        ∀ _ : ProjectivePlane P L, ∃ S : Set P, ∀ l : L,
+          1 ≤ (S ∩ {p : P | p ∈ l}).ncard ∧ (S ∩ {p : P | p ∈ l}).ncard ≤ C := by
+  sorry
+
+end Erdos1159

FormalConjectures/ErdosProblems/1206.lean

@@ -0,0 +1,53 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1206
+
+*References:*
+- [erdosproblems.com/1206](https://www.erdosproblems.com/1206)
+- [Er80] Erdős, Paul, *A survey of problems in combinatorial number theory*. Ann. Discrete Math.
+  (1980), 89-115.
+- [GGK26] M. Garaev, F. Garayev, and S. Konyagin, *On Sidon sets with squares, cubes, and quartics
+  in short intervals*. arXiv:2602.08807 (2026).
+- [GaKo24] Gabdullin, M. R. and Konyagin, S. V., *Trigonometric polynomials with frequencies in the
+  set of cubes*. Math. Notes (2024), 336--340.
+-/
+
+namespace Erdos1206
+
+/--
+Does $\{1,2^3,\ldots,N^3\}$ contain a Sidon set of size $\gg N$?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_1206.parts.i : answer(sorry) ↔
+    ∃ c : ℝ, 0 < c ∧ ∀ᶠ N in Filter.atTop, ∃ S : Finset ℕ,
+      S ⊆ (Finset.Icc 1 N).image (fun n => n ^ 3) ∧
+      IsSidon (S : Set ℕ) ∧ c * (N : ℝ) ≤ (S.card : ℝ) := by
+  sorry
+
+/--
+Is there an infinite set $A\subset \mathbb{N}$ of positive density such that $\{a^3 : a\in A\}$ is a Sidon set?
+-/
+@[category research open, AMS 5 11]
+theorem erdos_1206.parts.ii : answer(sorry) ↔
+    ∃ A : Set ℕ, A.Infinite ∧ 0 < A.lowerDensity ∧
+      IsSidon ((fun a : ℕ => a ^ 3) '' A) := by
+  sorry
+
+end Erdos1206

FormalConjectures/ErdosProblems/1207.lean

@@ -0,0 +1,53 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 1207
+
+*References:*
+- [erdosproblems.com/1207](https://www.erdosproblems.com/1207)
+- [BMP05] Brass, Peter and Moser, William and Pach, János, *Research problems in discrete geometry*.
+  (2005), xii+499.
+- [Er80] Erdős, Paul, *A survey of problems in combinatorial number theory*. Ann. Discrete Math.
+  (1980), 89-115.
+- [PaTa02] Pach, János and Tardos, Gábor, *Isosceles triangles determined by a planar point set*.
+  Graphs Combin. (2002), 769--779.
+-/
+
+open Filter
+open scoped EuclideanGeometry
+
+namespace Erdos1207
+
+/--
+`P d n` is the largest number $m$ such that every set of $n$ points in $\mathbb{R}^d$ has an
+isosceles-free subset of size at least $m$.
+-/
+noncomputable def P (d n : ℕ) : ℕ :=
+  sInf {m : ℕ | ∃ S : Finset (ℝ^d), S.card = n ∧
+    m = sSup {k : ℕ | ∃ A ⊆ S, (A : Set (ℝ^d)).IsIsoscelesFree ∧ A.card = k}}
+
+/--
+Let $P_d(n)$ be such that in any set of $n$ points in $\mathbb{R}^d$ there exist at least $P_d(n)$ many points which do not contain an isosceles triangle. Estimate $P_d(n)$ - in particular, is it true that $$P_2(n)<n^{1-c}$$ for some constant $c>0$?
+-/
+@[category research open, AMS 52]
+theorem erdos_1207 : answer(sorry) ↔
+    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (P 2 n : ℝ) < (n : ℝ) ^ (1 - c) := by
+  sorry
+
+end Erdos1207

FormalConjectures/ErdosProblems/181.lean

@@ -0,0 +1,48 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+
+import FormalConjecturesUtil
+
+/-!
+# Erdős Problem 181
+
+*References:*
+- [erdosproblems.com/181](https://www.erdosproblems.com/181)
+- [Er93] Erdős, Paul, *Some of my favorite solved and unsolved problems in graph theory*.
+  Quaestiones Math. (1993), 333-350.
+- [Ti22] Tikhomirov, K., *A remark on the Ramsey number of the hypercube*. arXiv:2208.14568 (2022).
+-/
+
+namespace Erdos181
+
+open SimpleGraph
+
+/-- The diagonal Ramsey number of a finite graph `G`: the least `N` such that every red-blue
+colouring of the edges of the complete graph on `N` vertices contains a monochromatic copy of `G`.
+A graph `R` records the red edges, and `Rᶜ` records the blue edges. -/
+noncomputable def diagonalRamseyNumber {α : Type*} [Fintype α] (G : SimpleGraph α) : ℕ :=
+  sInf {N : ℕ | ∀ R : SimpleGraph (Fin N), G.IsContained R ∨ G.IsContained Rᶜ}
+
+/--
+Let $Q_n$ be the $n$-dimensional hypercube graph (so that $Q_n$ has $2^n$ vertices and $n2^{n-1}$ edges). Prove that $$R(Q_n) \ll 2^n.$$
+-/
+@[category research open, AMS 5]
+theorem erdos_181 :
+    ∃ C > (0 : ℝ), ∀ n : ℕ,
+      (diagonalRamseyNumber (hypercube n) : ℝ) ≤ C * 2 ^ n := by
+  sorry
+
+end Erdos181