feat(ErdosProblems): 6x probability-related formalizations

FormalConjectures/ErdosProblems/1144.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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 1144
+
+Let $f$ be a random completely multiplicative function, where for each prime $p$ we independently
+choose $f(p) \in \{-1, 1\}$ uniformly at random. Is it true that the limsup of
+$\sum_{m \leq N} f(m) / \sqrt{N}$ is infinite with probability 1?
+
+*Reference:* [erdosproblems.com/1144](https://www.erdosproblems.com/1144)
+
+[Va99] Montgomery, H.L. and Vaughan, R.C., *Multiplicative Number Theory I: Classical Theory*.
+Cambridge Studies in Advanced Mathematics, Cambridge University Press, 2007.
+
+[At25] Atherfold, C., *Almost sure bounds for weighted sums of Rademacher random multiplicative
+functions*. arXiv:2501.11076, 2025.
+-/
+
+open MeasureTheory ProbabilityTheory Filter Finset BigOperators
+
+namespace Erdos1144
+
+/-- A random variable is Rademacher distributed: takes values $\pm 1$ with equal probability. -/
+def IsRademacher {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (X : Ω → ℝ) : Prop :=
+  (∀ ω, X ω = 1 ∨ X ω = -1) ∧
+  μ {ω | X ω = 1} = μ {ω | X ω = -1}
+
+/-- The random *completely* multiplicative function built from Rademacher signs at primes.
+For $n \geq 1$: $f(n) = \prod_{p \in \operatorname{primeFactors}(n)} \varepsilon(p)^{v_p(n)}$.
+For $n = 0$: $f(0) = 0$.
+This is completely multiplicative (as opposed to merely multiplicative, cf. Problem 520). -/
+noncomputable def randMultFun {Ω : Type*} (ε : ℕ → Ω → ℝ) (ω : Ω) (n : ℕ) : ℝ :=
+  if n = 0 then 0
+  else ∏ p ∈ n.factorization.support, (ε p ω) ^ (n.factorization p)
+
+/-- The partial sum $\sum_{m=1}^{N} f(m)$. -/
+noncomputable def partialSum {Ω : Type*} (ε : ℕ → Ω → ℝ) (ω : Ω) (N : ℕ) : ℝ :=
+  ∑ m ∈ Finset.Icc 1 N, randMultFun ε ω m
+
+/--
+Erdős Problem 1144 [Va99, 1.11]:
+
+Let $f$ be a random completely multiplicative function, where for each prime $p$
+we independently choose $f(p) \in \{-1, 1\}$ uniformly at random. Is it true that
+$$\limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N}} = \infty$$
+with probability 1?
+
+This model is sometimes called a Rademacher random multiplicative function.
+Atherfold [At25] proved that, almost surely,
+$$\sum_{m \leq N} f(m) \ll N^{1/2} (\log N)^{1+o(1)}.$$
+-/
+@[category research open, AMS 11 60]
+theorem erdos_1144 :
+    answer(sorry) ↔
+    ∀ (Ω : Type*) [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
+      (ε : ℕ → Ω → ℝ),
+      (∀ k, IsRademacher μ (ε k)) →
+      iIndepFun ε μ →
+      (∀ᵐ ω ∂μ, ∀ C : ℝ,
+        ∃ᶠ N in atTop,
+          partialSum ε ω N > C * Real.sqrt (N : ℝ)) := by
+  sorry
+
+end Erdos1144

FormalConjectures/ErdosProblems/1155.lean

@@ -0,0 +1,108 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 1155
+
+*Reference:* [erdosproblems.com/1155](https://www.erdosproblems.com/1155)
+
+Construct a random graph on $n$ vertices in the following way: begin with the complete graph
+$K_n$. At each stage, choose uniformly a random triangle in the graph and delete all the edges
+of this triangle. Repeat until the graph is triangle-free. If $f(n)$ is the number of edges
+remaining, is it true that $\mathbb{E}[f(n)] \asymp n^{3/2}$ and that $f(n) \ll n^{3/2}$
+almost surely?
+
+A problem of Bollobás and Erdős [Bo98, p.231][Va99, 3.61].
+
+Bohman, Frieze, and Lubetzky [BFL15] proved that $f(n) = n^{3/2 + o(1)}$ a.s.
+
+[Bo98] Bollobás, B., _Modern Graph Theory_, Graduate Texts in Mathematics 184, Springer (1998).
+
+[Va99] Vu, V. H. (1999), 3.61.
+
+[Gr97] Grable, D. A., _On random greedy triangle packing_, Electronic Journal of
+Combinatorics 4 (1997), Research Paper 11.
+
+[BFL15] Bohman, T., Frieze, A., and Lubetzky, E., _Random triangle removal_,
+Advances in Mathematics 280 (2015), 379--438.
+-/
+
+open SimpleGraph Filter
+
+open scoped Topology
+
+namespace Erdos1155
+
+/-- The triangle removal process on $K_n$: starting from the complete graph on $n$
+    vertices, repeatedly choose a uniformly random triangle and remove all three
+    of its edges, until the graph is triangle-free.
+
+    `triangleRemovalExpectedEdges n` is $\mathbb{E}[f(n)]$, the expected number of edges
+    remaining when the process terminates. -/
+opaque triangleRemovalExpectedEdges (n : ℕ) : ℝ
+
+/-- The probability that the number of edges remaining after the triangle
+    removal process on $K_n$ satisfies a given predicate $P$. -/
+opaque triangleRemovalEdgeProb (n : ℕ) (P : ℕ → Prop) : ℝ
+
+/--
+Erdős Problem #1155, Part 1 [Bo98, p.231]:
+
+$\mathbb{E}[f(n)] \asymp n^{3/2}$, i.e., there exist constants $c_1, c_2 > 0$ such that for all
+sufficiently large $n$, $c_1 \cdot n^{3/2} \leq \mathbb{E}[f(n)] \leq c_2 \cdot n^{3/2}$.
+-/
+@[category research open, AMS 5 60]
+theorem erdos_1155 : answer(sorry) ↔
+    ∃ c₁ c₂ : ℝ, 0 < c₁ ∧ 0 < c₂ ∧
+      ∃ N₀ : ℕ, ∀ n : ℕ, n ≥ N₀ →
+        c₁ * (n : ℝ) ^ ((3 : ℝ) / 2) ≤ triangleRemovalExpectedEdges n ∧
+        triangleRemovalExpectedEdges n ≤ c₂ * (n : ℝ) ^ ((3 : ℝ) / 2) := by
+  sorry
+
+/--
+Erdős Problem #1155, Part 2 [Bo98, p.231]:
+
+$f(n) \ll n^{3/2}$ almost surely, i.e., there exists $C > 0$ such that with
+probability tending to $1$, $f(n) \leq C \cdot n^{3/2}$.
+-/
+@[category research open, AMS 5 60]
+theorem erdos_1155.variants.almost_sure : answer(sorry) ↔
+    ∃ C : ℝ, 0 < C ∧
+      Tendsto (fun n : ℕ =>
+        triangleRemovalEdgeProb n (fun k => (k : ℝ) ≤ C * (n : ℝ) ^ ((3 : ℝ) / 2)))
+        atTop (nhds 1) := by
+  sorry
+
+/--
+Erdős Problem #1155, Variant (Bohman–Frieze–Lubetzky [BFL15]):
+
+$f(n) = n^{3/2 + o(1)}$ almost surely, i.e., for every $\varepsilon > 0$, the probability that
+$n^{3/2 - \varepsilon} \leq f(n) \leq n^{3/2 + \varepsilon}$ tends to $1$ as $n \to \infty$.
+This strengthens Part 2 by providing a matching almost-sure lower bound.
+-/
+@[category research solved, AMS 5 60]
+theorem erdos_1155.variants.bfl15 : answer(sorry) ↔
+    ∀ ε : ℝ, 0 < ε →
+      Tendsto (fun n : ℕ =>
+        triangleRemovalEdgeProb n (fun k =>
+          (n : ℝ) ^ ((3 : ℝ) / 2 - ε) ≤ (k : ℝ) ∧
+          (k : ℝ) ≤ (n : ℝ) ^ ((3 : ℝ) / 2 + ε)))
+        atTop (nhds 1) := by
+  sorry
+
+end Erdos1155

FormalConjectures/ErdosProblems/1156.lean

@@ -0,0 +1,99 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 1156
+
+*Reference:* [erdosproblems.com/1156](https://www.erdosproblems.com/1156)
+
+Let $G$ be a random graph on $n$ vertices, in which every edge is included
+independently with probability $1/2$ (the Erdős–Rényi model $G(n, 1/2)$).
+
+Bollobás [Bo88] proved that $\chi(G) \sim n / (2 \log_2 n)$ with high probability.
+Shamir and Spencer [ShSp87] proved concentration within $o(\sqrt{n})$.
+Heckel and Riordan [HeRi23] proved concentration cannot be within $n^c$ for $c < 1/2$.
+
+[AlSp92] Alon, N. and Spencer, J., _The Probabilistic Method_, Wiley, 1992.
+
+[AlSp16] Alon, N. and Spencer, J. H., _The Probabilistic Method_, 4th ed., Wiley, 2016.
+
+[Bo88] Bollobás, B., _The chromatic number of random graphs_. Combinatorica (1988), 49–55.
+
+[He21] Heckel, A., _Non-concentration of the chromatic number of a random graph_.
+J. Amer. Math. Soc. (2021), 245–260.
+
+[HeRi23] Heckel, A. and Riordan, O., _How does the chromatic number of a random graph vary?_
+J. Lond. Math. Soc. (2) (2023), 1769–1815.
+
+[Sc17] Scott, A., _On the concentration of the chromatic number of random graphs_.
+arXiv:0806.0178 (2017).
+
+[ShSp87] Shamir, E. and Spencer, J., _Sharp concentration of the chromatic number on random
+graphs $G_{n,p}$_. Combinatorica (1987), 121–129.
+
+[Va99] Vu, V. H. (1999), 3.64.
+-/
+
+open Filter
+
+open scoped Topology
+
+namespace Erdos1156
+
+/-- The probability that the chromatic number of a uniformly random graph
+$G(n, 1/2)$ on $n$ vertices satisfies predicate $P$. Here $G(n, 1/2)$ is the
+Erdős–Rényi model where each edge is included independently with
+probability $1/2$, equivalently the uniform distribution over all simple
+graphs on $n$ labelled vertices. -/
+opaque chromaticNumberProb (n : ℕ) (P : ℕ → Prop) : ℝ
+
+/--
+Erdős Problem 1156, Part 1 [AlSp92]:
+
+There exists a constant $C$ such that $\chi(G(n, 1/2))$ is almost surely concentrated
+on at most $C$ values. That is, for every $\varepsilon > 0$ and all sufficiently large $n$,
+there is a set $S$ of at most $C$ natural numbers with
+$\mathbb{P}(\chi(G) \in S) \geq 1 - \varepsilon$.
+-/
+@[category research open, AMS 5 60]
+theorem erdos_1156 :
+    ∃ C : ℕ, ∀ ε : ℝ, 0 < ε →
+      ∀ᶠ n in atTop,
+        ∃ S : Finset ℕ, S.card ≤ C ∧
+          chromaticNumberProb n (· ∈ S) ≥ 1 - ε := by
+  sorry
+
+/--
+Erdős Problem 1156, Part 2 [AlSp92] [Va99]:
+
+There exists a function $\omega : \mathbb{N} \to \mathbb{R}$ with $\omega(n) \to \infty$ such that
+for every function $f : \mathbb{N} \to \mathbb{R}$, for all sufficiently large $n$,
+$$
+\mathbb{P}(|\chi(G) - f(n)| < \omega(n)) < 1/2.
+$$
+That is, the chromatic number cannot be concentrated in any interval of width
+$2\omega(n)$ with probability $\geq 1/2$.
+-/
+@[category research open, AMS 5 60]
+theorem erdos_1156.variants.anticoncentration :
+    ∃ ω : ℕ → ℝ, Tendsto ω atTop atTop ∧
+      ∀ f : ℕ → ℝ, ∀ᶠ n in atTop,
+        chromaticNumberProb n (fun k => |(k : ℝ) - f n| < ω n) < 1 / 2 := by
+  sorry
+
+end Erdos1156