From e3b1173e63e20cfae5146620be789f81edd3b1c6 Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Fri, 5 Dec 2025 14:36:35 +0000 Subject: [PATCH 1/5] Formalized the statement of Erdos Problem 82 --- FormalConjectures/ErdosProblems/82.lean | 52 +++++++++++++++++++++++++ 1 file changed, 52 insertions(+) create mode 100644 FormalConjectures/ErdosProblems/82.lean diff --git a/FormalConjectures/ErdosProblems/82.lean b/FormalConjectures/ErdosProblems/82.lean new file mode 100644 index 000000000..3e418d25d --- /dev/null +++ b/FormalConjectures/ErdosProblems/82.lean @@ -0,0 +1,52 @@ +/- +Copyright 2025 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 FormalConjectures.Util.ProblemImports + +/-! +# Erdős Problem 82 + +*Reference:* [erdosproblems.com/82](https://www.erdosproblems.com/82) +-/ + +open Classical SimpleGraph Filter + +namespace Erdos82 + +variable {V : Type*} [Fintype V] + +/-- +A predicate that holds if $S$ is a regular induced subgraph of $G$ +-/ +def IsRegularInduced {G : SimpleGraph V} (S : Subgraph G) : Prop := + S.IsInduced ∧ ∃ k, (S.coe).IsRegularOfDegree k + +/-- +$F(n)$ is the maximal integer such that every graph on $n$ vertices +contains a regular induced subgraph on at least $F(n)$ vertices. +-/ +noncomputable def F (n : ℕ) : ℕ := + sSup { k | ∀ (G : SimpleGraph (Fin n)), ∃ S : Subgraph G, + IsRegularInduced S ∧ S.verts.ncard = k} + +/-- +$F(n) / \log n \to \infty as n \to \infty$ +-/ +@[category research open, AMS 5] +theorem erdos_82 : Tendsto (fun n => F n / Real.log n) atTop atTop := by + sorry + +end Erdos82 From 95fd02f5aada75cf219cea337f9e078ae711967c Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Mon, 15 Dec 2025 17:36:56 +0000 Subject: [PATCH 2/5] Add variant - `F_upper_bound` --- FormalConjectures/ErdosProblems/82.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/FormalConjectures/ErdosProblems/82.lean b/FormalConjectures/ErdosProblems/82.lean index 3e418d25d..530cf1c33 100644 --- a/FormalConjectures/ErdosProblems/82.lean +++ b/FormalConjectures/ErdosProblems/82.lean @@ -49,4 +49,12 @@ $F(n) / \log n \to \infty as n \to \infty$ theorem erdos_82 : Tendsto (fun n => F n / Real.log n) atTop atTop := by sorry +/-- +$F(n) \le O(n^{1/2} \ln ^ {3/4} n)$ +-/ +@[category research solved, AMS 5] +theorem erdos_82.variants.F_upper_bound : + (fun n => (F n : ℝ)) =O[atTop] (fun n => Real.sqrt n * (Real.log n) ^ (3 / 4)) := by + sorry + end Erdos82 From 85fa4e3158c441ad6c97cb3ff5d54394123756e8 Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Mon, 15 Dec 2025 21:03:29 +0000 Subject: [PATCH 3/5] Add reference to docstring of `erdos_82.variants.F_upper_bound` --- FormalConjectures/ErdosProblems/82.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/FormalConjectures/ErdosProblems/82.lean b/FormalConjectures/ErdosProblems/82.lean index 530cf1c33..9e465b97c 100644 --- a/FormalConjectures/ErdosProblems/82.lean +++ b/FormalConjectures/ErdosProblems/82.lean @@ -51,6 +51,10 @@ theorem erdos_82 : Tendsto (fun n => F n / Real.log n) atTop atTop := by /-- $F(n) \le O(n^{1/2} \ln ^ {3/4} n)$ + +Theorem 1.4 from [AKS07] + +[AKS07] Alon, N. and Krivelevich, M. and Sudakov, B., Large nearly regular induced subgraphs. arXiv:0710.2106 (2007). -/ @[category research solved, AMS 5] theorem erdos_82.variants.F_upper_bound : From 7052f758fdc0547115b00e7878748aac99a3c7a1 Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Tue, 16 Dec 2025 18:47:53 +0000 Subject: [PATCH 4/5] Improve formatting and formalization of `F n` --- FormalConjectures/ErdosProblems/82.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/ErdosProblems/82.lean b/FormalConjectures/ErdosProblems/82.lean index 9e465b97c..a59249991 100644 --- a/FormalConjectures/ErdosProblems/82.lean +++ b/FormalConjectures/ErdosProblems/82.lean @@ -39,8 +39,8 @@ $F(n)$ is the maximal integer such that every graph on $n$ vertices contains a regular induced subgraph on at least $F(n)$ vertices. -/ noncomputable def F (n : ℕ) : ℕ := - sSup { k | ∀ (G : SimpleGraph (Fin n)), ∃ S : Subgraph G, - IsRegularInduced S ∧ S.verts.ncard = k} + sSup {k | ∀ (G : SimpleGraph (Fin n)), ∃ S : Subgraph G, + IsRegularInduced S ∧ k ≤ S.verts.ncard} /-- $F(n) / \log n \to \infty as n \to \infty$ From 2e1cf3c895f71beca8b4d4198b3fb7afa277a9f8 Mon Sep 17 00:00:00 2001 From: "Malhar A. Patel" Date: Thu, 18 Dec 2025 19:32:55 +0000 Subject: [PATCH 5/5] =?UTF-8?q?Fix=20type=20of=20`3=20/=204`=20to=20`?= =?UTF-8?q?=E2=84=9D`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- FormalConjectures/ErdosProblems/82.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/82.lean b/FormalConjectures/ErdosProblems/82.lean index a59249991..b9d27d381 100644 --- a/FormalConjectures/ErdosProblems/82.lean +++ b/FormalConjectures/ErdosProblems/82.lean @@ -58,7 +58,7 @@ Theorem 1.4 from [AKS07] -/ @[category research solved, AMS 5] theorem erdos_82.variants.F_upper_bound : - (fun n => (F n : ℝ)) =O[atTop] (fun n => Real.sqrt n * (Real.log n) ^ (3 / 4)) := by + (fun n => (F n : ℝ)) =O[atTop] (fun n => Real.sqrt n * (Real.log n) ^ (3 / 4 : ℝ)) := by sorry end Erdos82