Erdős Problem 1158 to Erdős Problem 1180

TheoremErdős Problem 1158#

References: - erdosproblems.com/1158 - [Er64f] Erdős, P., On extremal problems of graphs and generalized graphs. Israel J. Math. (1964), 183--190.

Quoted from FormalConjectures/ErdosProblems/1158.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1158.

The file states 1 research or textbook statement: 1 open.

Erdos1158.erdos_1158

Open: stated without proof.

Let \(K_{t}(r)\) be the complete \(t\)-partite \(t\)-uniform hypergraph with \(r\) vertices in each class. Is it true that

\[\mathrm{ex}_t(n,K_t(r)) \geq n^{t-r^{1-t}-o(1)}\]

for all \(t,r\geq 2\)? The restriction \(r\geq 2\) excludes forbidding a single edge.

theorem erdos_1158 :
    ∀ t r : ℕ, 2 ≤ t → 2 ≤ r →
    ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop,
      (n : ℝ) ^ ((t : ℝ) - (r : ℝ) ^ (1 - (t : ℝ)) - ε) ≤
        (Hypergraph.partiteExtremalNumber n t r : ℝ)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1158.lean, line 42.

Sources

• FormalConjectures/ErdosProblems/1158.lean at 2055e5ad
• erdosproblems.com/1158

LeanErdos1158.erdos_1158

TheoremErdős Problem 1159#

References: - 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.

Quoted from FormalConjectures/ErdosProblems/1159.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1159.

The file states 1 research or textbook statement: 1 open.

Erdos1159.erdos_1159

Open: stated without proof.

Determine whether there exists a constant \(C>1\) such that the following holds.

Let \(P\) be a finite 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\)?

theorem erdos_1159 :
    ∃ 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

Category research open; AMS 05 Combinatorics, 51 Geometry. Declared in FormalConjectures/ErdosProblems/1159.lean, line 43.

Sources

• FormalConjectures/ErdosProblems/1159.lean at 2055e5ad
• erdosproblems.com/1159

LeanErdos1159.erdos_1159

TheoremErdős Problem 1160#

References: - erdosproblems.com/1160 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [BNV07] Blackburn, S. R., Neumann, P. M. and Venkataraman, G., Enumeration of finite groups. Cambridge Tracts in Mathematics 173, Cambridge University Press (2007), xii+281. - [Pa03] Pantelidakis, I., On the Number of Non-isomorphic Groups of the Same Order. DPhil thesis, University of Oxford (2003).

Quoted from FormalConjectures/ErdosProblems/1160.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1160.

The file states 2 research or textbook statements: 2 open. It also has 1 test statement, counted here but not shown.

Erdos1160.erdos_1160

Open: stated without proof.

Let \(g(n)\) denote the number of groups of order \(n\). If \(n\leq 2^m\) then \(g(n)\leq g(2^m)\).

This is [Va99, 5.71] and an open problem (Question 22.16) in [BNV07], where its origin could not be traced. It has been attributed to Erdős, Higman and others. Pantelidakis [Pa03] proved it for odd \(n\) and \(m\geq 3619\).

It is a conjecture, not a question. We take \(n\geq 1\); for \(n=0\) it holds trivially, since \(g(0)=0\).

theorem erdos_1160 : ∀ n m : ℕ, 0 < n → n ≤ 2 ^ m → g n ≤ g (2 ^ m)

Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1160.lean, line 72.

Erdos1160.erdos_1160.variants.sum

Open: stated without proof.

Question 22.18 of [BNV07] suggests the even stronger conjecture

\[\sum_{n<2^m}g(n) \leq g(2^m)\]

for all sufficiently large \(m\) (perhaps even as soon as \(m\geq 7\)).

The sum is over \(1\leq n<2^m\).

theorem erdos_1160.variants.sum :
    ∀ᶠ m : ℕ in atTop, ∑ n ∈ Finset.Ico 1 (2 ^ m), g n ≤ g (2 ^ m)

Category research open; AMS 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1160.lean, line 81.

Sources

• FormalConjectures/ErdosProblems/1160.lean at 2055e5ad
• erdosproblems.com/1160

LeanErdos1160.erdos_1160 · Erdos1160.erdos_1160.variants.sum

TheoremErdős Problem 1161#

References: - erdosproblems.com/1161 - [Be25d] Beker, Adrian, The most probable order of a random permutation. arXiv:2510.11698 (2025). - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).

Quoted from FormalConjectures/ErdosProblems/1161.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1161.

The file states 3 research or textbook statements: 3 solved. It also has 2 API statements, counted here but not shown.

Erdos1161.erdos_1161

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1161.lean#L50.

Let \(f_k(n)\) count the number of elements of \(S_n\) of order \(k\). For which values of \(k\) will \(f_k(n)\) be maximal? [Va99, 5.72]

Beker [Be25d, Theorem 1.2] proved that, for all large \(n\), \(f_k(n)\) is maximal if and only if \(k\geq 1\) is minimal such that \([1,\ldots,n-k]\mid k\), where \([\cdot]\) is the least common multiple. The last clause on erdosproblems.com/1161 reads "\(f_k(n)=(n-1)!\)" instead of "\(f_k(n)\) is maximal"; we follow [Be25d]. For \(k > n\) we read \(n-k\) as \(0\), which does not change the least such \(k\), because \(k = n\) qualifies.

theorem erdos_1161 :
    ∀ᶠ n : ℕ in atTop, {k : ℕ | ∀ j : ℕ, f j n ≤ f k n} = erdos_1161.answer n

Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1161.lean, line 78.

Erdos1161.erdos_1161.variants.max_asymptotic

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1161.lean#L50.

Beker [Be25d, Theorem 1.1] proved that

\[\max_{k\geq 1} f_k(n)\sim (n-1)!.\]

theorem erdos_1161.variants.max_asymptotic :
    (fun n : ℕ ↦ (maxF n : ℝ)) ~[atTop] (fun n : ℕ ↦ ((n - 1).factorial : ℝ))

Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1161.lean, line 89.

Erdos1161.erdos_1161.variants.threshold

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1161.lean#L50.

Beker [Be25d, Theorem 1.1] also proved that, if \(n\) is sufficiently large and \(f_k(n)\geq (n-1)!\), then \([1,\ldots,n-k]\mid k\). The statement also records \(1\leq k\leq n\), since [Be25d] writes such \(k\) as \(n-k'\) with \(0\leq k'\leq n-1\).

theorem erdos_1161.variants.threshold :
    ∀ᶠ n : ℕ in atTop, ∀ k : ℕ, (n - 1).factorial ≤ f k n →
      k ≤ n ∧ 0 < k ∧ Nat.lcmUpto (n - k) ∣ k

Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1161.lean, line 101.

Sources

• FormalConjectures/ErdosProblems/1161.lean at 2055e5ad
• erdosproblems.com/1161

LeanErdos1161.erdos_1161 · Erdos1161.erdos_1161.variants.max_asymptotic · Erdos1161.erdos_1161.variants.threshold

TheoremErdős Problem 1162#

References: - erdosproblems.com/1162 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [Py93] Pyber, L., Asymptotic results for permutation groups. Groups and computation (New Brunswick, NJ, 1991), DIMACS Ser. Discrete Math. Theoret. Comput. Sci. 11 (1993), 197-219. - [RoTr25] Roney-Dougal, C. M. and Tracey, G., Subgroups of symmetric groups: enumeration and asymptotic properties. arXiv:2503.05416 (2025).

Quoted from FormalConjectures/ErdosProblems/1162.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1162.

The file states 4 research or textbook statements: 1 open and 3 solved. It also has 1 API statement, counted here but not shown.

Erdos1162.erdos_1162

Open: stated without proof.

Give an asymptotic formula for the number of subgroups of \(S_n\). Is there a statistical theorem on their order?

A problem of Erdős and Turán [Va99, 5.73]. We state the first question: erdos_1162.answer is a function asymptotically equivalent to the number \(f(n)\) of subgroups of \(S_n\) (an explicit formula is intended, not \(f\) itself). The second question is too vague to state.

theorem erdos_1162 :
    (fun n : ℕ ↦ (f n : ℝ)) ~[atTop] erdos_1162.answer

Category research open; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1162.lean, line 61.

Erdos1162.erdos_1162.variants.pyber

Solved: stated here without proof.

Pyber [Py93] proved that

\[\log f(n)\asymp n^2.\]

theorem erdos_1162.variants.pyber :
    (fun n : ℕ ↦ Real.log (f n : ℝ)) =Θ[atTop] fun n : ℕ ↦ (n : ℝ) ^ 2

Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1162.lean, line 70.

Erdos1162.erdos_1162.variants.roney_dougal_tracey

Solved: stated here without proof.

Roney-Dougal and Tracey [RoTr25] have proved that

\[\log f(n)=\left(\frac{1}{16}+o(1)\right)n^2.\]

Here \(\log\) is the logarithm to base \(2\), as in [RoTr25].

theorem erdos_1162.variants.roney_dougal_tracey :
    (fun n : ℕ ↦ Real.logb 2 (f n : ℝ)) ~[atTop] fun n : ℕ ↦ (n : ℝ) ^ 2 / 16

Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1162.lean, line 80.

Erdos1162.erdos_1162.variants.roney_dougal_tracey_bounds

Solved: stated here without proof.

Roney-Dougal and Tracey [RoTr25, Theorem 1] proved that there are absolute constants \(\alpha>0\) and \(\beta\) such that for all integers \(n>1\)

\[2^{n^2/16+\alpha n\log n}\leq f(n)\leq 2^{n^2/16+\beta n^{3/2}},\]

where \(\log\) is the logarithm to base \(2\). This implies the previous variant.

theorem erdos_1162.variants.roney_dougal_tracey_bounds :
    ∃ α > (0 : ℝ), ∃ β : ℝ, ∀ n : ℕ, 1 < n →
      (2 : ℝ) ^ ((n : ℝ) ^ 2 / 16 + α * n * Real.logb 2 n) ≤ f n ∧
        (f n : ℝ) ≤ (2 : ℝ) ^ ((n : ℝ) ^ 2 / 16 + β * (n : ℝ) ^ ((3 : ℝ) / 2))

Category research solved; AMS 05 Combinatorics, 20 Group theory and generalizations. Declared in FormalConjectures/ErdosProblems/1162.lean, line 91.

Sources

• FormalConjectures/ErdosProblems/1162.lean at 2055e5ad
• erdosproblems.com/1162

LeanErdos1162.erdos_1162 · Erdos1162.erdos_1162.variants.pyber · Erdos1162.erdos_1162.variants.roney_dougal_tracey · Erdos1162.erdos_1162.variants.roney_dougal_tracey_bounds

TheoremErdős Problem 1164#

References: - erdosproblems.com/1164 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [ErTa60] Erdős, P. and Taylor, S. J., Some problems concerning the structure of random walk paths. Acta Math. Acad. Sci. Hungar. 11 (1960), 137--162. PDF - [Re90] Révész, P., Random walk in random and non-random environments. World Scientific, Singapore (1990). - [DPRZ04] Dembo, A., Peres, Y., Rosen, J. and Zeitouni, O., Cover times for Brownian motion and random walks in two dimensions. Ann. of Math. (2) 160 (2004), 433--464. arXiv:math/0107191

Quoted from FormalConjectures/ErdosProblems/1164.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1164.

The file states 2 research or textbook statements: 2 solved. It also has 1 API statement, counted here but not shown.

Erdos1164.erdos_1164

Solved: stated here without proof.

Let \(R_n\) be the maximal integer such that almost every random walk from the origin in \(\mathbb{Z}^2\) visits every \(x\in\mathbb{Z}^2\) with \(\lVert x\rVert\leq R_n\) in at most \(n\) steps.

Is it true that

\[\log R_n \asymp \sqrt{\log n}?\]

A problem of Erdős and Taylor, see [ErTa60, p. 153] and [Va99, 6.76]. This is true, as proved independently by Révész [Re90] and Kesten, see [DPRZ04, Section 1.3], which reports that they proved the following. The probability that the disc of radius \(n\) is covered by time \(e^{t(\log n)^2}\) has \(\liminf_{n\to\infty}\) at least \(e^{-b/t}\) and \(\limsup_{n\to\infty}\) at most \(e^{-a/t}\) for every \(t>0\), where \(0\lt a\lt b\lt \infty\) are constants. The exact limit is in erdos_1164.variants.dembo_peres_rosen_zeitouni.

We take the simple random walk (IsSimpleRandomWalkSteps). Read literally, \(R_n\) would be \(0\): for every \(n\) some walk misses a neighbour of the origin, and such walks have positive probability. So \(R_n=R_n(\omega)\) is the random variable coveringRadius, and \(\log R_n\asymp\sqrt{\log n}\) means tightness: for every \(\varepsilon>0\) there are constants \(c>0\) and \(C\) such that \(c\sqrt{\log n}\leq\log R_n\leq C\sqrt{\log n}\) with probability at least \(1-\varepsilon\) for all large \(n\). This is the sense of the results above and of erdos_1164.variants.dembo_peres_rosen_zeitouni, which are about probabilities, not almost sure bounds. [ErTa60, p. 153] asks an almost sure question about the time needed to cover the disc of radius \(n\); we follow the results in probability reported in [DPRZ04, Section 1.3].

theorem erdos_1164 {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
    {X : ℕ → Ω → ℤ × ℤ} (hX : IsSimpleRandomWalkSteps X) :
    ∀ ε : ℝ, 0 < ε → ∃ c C : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
      1 - ε ≤ (ℙ {ω | c * Real.sqrt (Real.log n) ≤ Real.log (coveringRadius X n ω) ∧
        Real.log (coveringRadius X n ω) ≤ C * Real.sqrt (Real.log n)}).toReal

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1164.lean, line 111.

Erdos1164.erdos_1164.variants.dembo_peres_rosen_zeitouni

Solved: stated here without proof.

Dembo, Peres, Rosen and Zeitouni [DPRZ04, Theorem 1.4] proved a conjecture of Kesten and Révész: if \(T_n\) is the time it takes the simple random walk in \(\mathbb{Z}^2\) to cover the disc of radius \(n\), then

\[\lim_{n\to\infty}\mathbb{P}\left(\log T_n\leq t(\log n)^2\right)=e^{-4/t}\]

for every \(t>0\).

The disc is \(D_n=D(0,n)\cap\mathbb{Z}^2\) (openDisc). Since \(T_n\) is an integer, \(\log T_n\leq t(\log n)^2\) holds if and only if \(T_n\leq\lfloor e^{t(\log n)^2}\rfloor\), that is, if the disc is covered by that time.

theorem erdos_1164.variants.dembo_peres_rosen_zeitouni {Ω : Type*} [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)] {X : ℕ → Ω → ℤ × ℤ}
    (hX : IsSimpleRandomWalkSteps X) (t : ℝ) (ht : 0 < t) :
    Tendsto (fun n : ℕ ↦
      (ℙ {ω | Covers X ⌊Real.exp (t * Real.log n ^ 2)⌋₊ ω (openDisc n)}).toReal)
      atTop (𝓝 (Real.exp (-4 / t)))

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1164.lean, line 130.

Sources

• FormalConjectures/ErdosProblems/1164.lean at 2055e5ad
• erdosproblems.com/1164

LeanErdos1164.erdos_1164 · Erdos1164.erdos_1164.variants.dembo_peres_rosen_zeitouni

TheoremErdős Problem 1165#

References: - erdosproblems.com/1165 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [HLOZ24] Hao, C., Li, X., Okada, I. and Zheng, Y., Favorite sites for simple random walk in two and more dimensions. arXiv:2409.00995 (2024). - [To01] Tóth, B., No more than three favorite sites for simple random walk. Ann. Probab. 29 (2001), 484--503.

Quoted from FormalConjectures/ErdosProblems/1165.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1165.

The file states 2 research or textbook statements: 2 solved. It also has 2 API statements, counted here but not shown.

Erdos1165.erdos_1165

Solved: stated here without proof.

Given a random walk \(s_0,s_1,\ldots\) in \(\mathbb{Z}^2\), starting at the origin, let \(f_n(x)\) count the number of \(0\leq k\leq n\) such that \(s_k=x\).

Let

\[F(n)=\{ x: f_n(x) = \max_y f_n(y)\}\]

be the set of 'favourite values'. Find

\[\mathbb{P}(\lvert F(n)\rvert=r\textrm{ infinitely often})\]

for \(r\geq 3\).

A problem of Erdős and Révész [Va99, 6.77]. We take the simple random walk, on any probability space (IsSimpleRandomWalkSteps). Hao, Li, Okada and Zheng [HLOZ24, Theorem 1.1] showed that the probability is \(1\) for \(r=3\) and \(0\) for \(r\geq 4\), see erdos_1165.variants.hao_li_okada_zheng. The value of erdos_1165.answer for \(r<3\) is not used.

theorem erdos_1165 {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
    {X : ℕ → Ω → ℤ × ℤ} (hX : IsSimpleRandomWalkSteps X) (r : ℕ) (hr : 3 ≤ r) :
    ℙ {ω | ∃ᶠ n in atTop, (favouriteSites X n ω).encard = (r : ℕ∞)} = erdos_1165.answer r

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1165.lean, line 98.

Erdos1165.erdos_1165.variants.hao_li_okada_zheng

Solved: stated here without proof.

Hao, Li, Okada and Zheng [HLOZ24, Theorem 1.1] proved that, for the simple random walk on \(\mathbb{Z}^2\), almost surely

\[\limsup_{n\to\infty} \#K^{(2)}(n) = 3,\]

where \(K^{(2)}(n)\) is the set of favourite sites at time \(n\). The cardinalities are natural numbers, so almost surely there are eventually at most three favourite sites, and exactly three infinitely often. Tóth [To01] proved the corresponding bound for the one-dimensional walk, see [HLOZ24, Section 1].

theorem erdos_1165.variants.hao_li_okada_zheng {Ω : Type*} [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)] {X : ℕ → Ω → ℤ × ℤ} (hX : IsSimpleRandomWalkSteps X) :
    ∀ᵐ ω, limsup (fun n ↦ (favouriteSites X n ω).encard) atTop = 3

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1165.lean, line 113.

Sources

• FormalConjectures/ErdosProblems/1165.lean at 2055e5ad
• erdosproblems.com/1165

LeanErdos1165.erdos_1165 · Erdos1165.erdos_1165.variants.hao_li_okada_zheng

TheoremErdős Problem 1166#

References: - erdosproblems.com/1166 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [ErTa60] Erdős, P. and Taylor, S. J., Some problems concerning the structure of random walk paths. Acta Math. Acad. Sci. Hungar. 11 (1960), 137--162. PDF - [DPRZ01] Dembo, A., Peres, Y., Rosen, J. and Zeitouni, O., Thick points for planar Brownian motion and the Erdős-Taylor conjecture on random walk. Acta Math. 186 (2001), 239--270. doi:10.1007/BF02401841 - [HLOZ24] Hao, C., Li, X., Okada, I. and Zheng, Y., Favorite sites for simple random walk in two and more dimensions. arXiv:2409.00995 (2024).

Quoted from FormalConjectures/ErdosProblems/1166.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1166.

The file states 3 research or textbook statements: 3 solved. It also has 2 API statements, counted here but not shown.

Erdos1166.erdos_1166

Solved: stated here without proof.

Given a random walk \(s_0,s_1,\ldots\) in \(\mathbb{Z}^2\), starting at the origin, let \(f_k(x)\) count the number of \(0\leq l\leq k\) such that \(s_l=x\).

Let

\[F(k)=\{ x: f_k(x) = \max_y f_k(y)\}\]

be the set of 'favourite values'. Is it true that

\[\left\lvert \bigcup_{k\leq n}F(k)\right\rvert \leq (\log n)^{O(1)}\]

almost surely, for all but finitely many \(n\)?

A problem of Erdős and Révész [Va99, 6.78]. The answer is yes. Almost surely there are at most three favourite sites at all large times [HLOZ24, Theorem 1.1], see Erdos1165.erdos_1165.variants.hao_li_okada_zheng, and the maximal local time is \(O((\log n)^2)\) [ErTa60, p. 162], see erdos_1166.variants.erdos_taylor. A favourite site stays a favourite site for as long as the maximal local time does not change. So for each value of the maximal local time, the sites that are favourite at some time while it has that value are all favourite at the last such time, and there are at most three of them, up to finitely many exceptions. This gives the bound \(O((\log n)^2)\) stated on the problem page.

We take the simple random walk (IsSimpleRandomWalkSteps). We read \(O(1)\) as a single exponent C that works for almost every walk. The cardinality is Set.encard, so an infinite union would not satisfy the bound.

theorem erdos_1166 {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
    {X : ℕ → Ω → ℤ × ℤ} (hX : IsSimpleRandomWalkSteps X) :
    ∃ C : ℕ, ∀ᵐ ω, ∀ᶠ n : ℕ in atTop,
      ((⋃ k ≤ n, favouriteSites X k ω).encard : ℝ≥0∞) ≤ ENNReal.ofReal (Real.log n ^ C)

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1166.lean, line 105.

Erdos1166.erdos_1166.variants.erdos_taylor

Solved: stated here without proof.

Erdős and Taylor [ErTa60, p. 162] proved that, for the simple random walk on \(\mathbb{Z}^2\), if \(T_n\) is the maximal number of visits to a point in the first \(n\) steps, then almost surely

\[\frac{1}{4\pi}\leq\liminf_{n\to\infty}\frac{T_n}{(\log n)^2} \leq\limsup_{n\to\infty}\frac{T_n}{(\log n)^2}\leq\frac{1}{\pi}.\]

They conjectured that the limit exists and equals \(1/\pi\), see erdos_1166.variants.dembo_peres_rosen_zeitouni.

We use maxLocalTime, which also counts the visit at time \(0\). This changes \(T_n\) by at most one. The bounds are stated with \(\varepsilon\) to avoid the junk values of liminf and limsup.

theorem erdos_1166.variants.erdos_taylor {Ω : Type*} [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)] {X : ℕ → Ω → ℤ × ℤ}
    (hX : IsSimpleRandomWalkSteps X) :
    ∀ᵐ ω, ∀ ε : ℝ, 0 < ε →
      (∀ᶠ n : ℕ in atTop, 1 / (4 * π) - ε ≤ (maxLocalTime X n ω : ℝ) / Real.log n ^ 2) ∧
      (∀ᶠ n : ℕ in atTop, (maxLocalTime X n ω : ℝ) / Real.log n ^ 2 ≤ 1 / π + ε)

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1166.lean, line 123.

Erdos1166.erdos_1166.variants.dembo_peres_rosen_zeitouni

Solved: stated here without proof.

Dembo, Peres, Rosen and Zeitouni [DPRZ01, Theorem 1.1] proved the conjecture of Erdős and Taylor: for the simple random walk on \(\mathbb{Z}^2\), if \(T_n^*\) is the maximal number of visits to a point in the first \(n\) steps, then almost surely

\[\lim_{n\to\infty}\frac{T_n^*}{(\log n)^2}=\frac{1}{\pi}.\]

maxLocalTime counts the visit at time \(0\). Whether this visit is counted changes \(T_n^*\) by at most one, so the limit is the same.

theorem erdos_1166.variants.dembo_peres_rosen_zeitouni {Ω : Type*} [MeasureSpace Ω]
    [IsProbabilityMeasure (ℙ : Measure Ω)] {X : ℕ → Ω → ℤ × ℤ}
    (hX : IsSimpleRandomWalkSteps X) :
    ∀ᵐ ω, Tendsto (fun n : ℕ ↦ (maxLocalTime X n ω : ℝ) / Real.log n ^ 2) atTop (𝓝 (1 / π))

Category research solved; AMS 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/1166.lean, line 141.

Sources

• FormalConjectures/ErdosProblems/1166.lean at 2055e5ad
• erdosproblems.com/1166

LeanErdos1166.erdos_1166 · Erdos1166.erdos_1166.variants.erdos_taylor · Erdos1166.erdos_1166.variants.dembo_peres_rosen_zeitouni

TheoremErdős Problem 1167#

References: - erdosproblems.com/1167 - [EHMR84] P. Erdős, A. Hajnal, A. Máté and R. Rado, Combinatorial set theory: partition relations for cardinals. Studies in Logic and the Foundations of Mathematics 106, North-Holland (1984).

The original Erdős–Hajnal problem list gives the additional conditions \(\gamma \geq 2\), \(r < \omega\), and \(\kappa_\alpha > r\). Without \(\gamma \geq 2\), the statement is false: taking \(\gamma = 1\) and \(\kappa_0 = \aleph_1\) with \(\lambda = \aleph_0\) gives a counterexample, since the partition relation with one color degenerates to a cardinality comparison (see erdos_1167.unrestricted_is_false). Without \(\kappa_\alpha > r\) it is also false: with \(r = 2\), \(\lambda = \aleph_0\) and targets \((2, \aleph_1)\), the premise \(2^{\aleph_0} \to (3, \aleph_1)^3\) holds, but a constant colouring of the pairs of \(\aleph_0\) has neither a red pair nor a blue set of size \(\aleph_1\).

Quoted from FormalConjectures/ErdosProblems/1167.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1167.

The file states 5 research or textbook statements: 4 open and 1 solved. It also has 2 test statements and 1 API statement, counted here but not shown.

Erdos1167.erdos_1167

Open: stated without proof.

Erdős Problem 1167. Let \(r \geq 2\) be finite, \(\gamma \geq 2\), and \(\lambda\) be an infinite cardinal. Let \(\kappa_\alpha > r\) be cardinals for all \(\alpha < \gamma\). Is it true that

\[2^\lambda \to (\kappa_\alpha + 1)_{\alpha < \gamma}^{r+1}\]

implies

\[\lambda \to (\kappa_\alpha)_{\alpha < \gamma}^r?\]

Here \(+\) means cardinal addition, so that \(\kappa_\alpha + 1 = \kappa_\alpha\) if \(\kappa_\alpha\) is infinite.

A problem of Erdős, Hajnal, and Rado.

theorem erdos_1167 :
    ∀ (r : ℕ), 2 ≤ r →
    ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam →
    ∀ (γ : Ordinal.{u}), 2 ≤ γ →
    ∀ (κ : γ.ToType → Cardinal.{u}), (∀ α, (r : Cardinal.{u}) < κ α) →
      cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) →
      cardinalPartitionRel lam r γ κ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1167.lean, line 59.

Erdos1167.erdos_1167.variants.finite_targets

Solved: stated here; a Lean proof is at https://github.com/mnn31/erdos-lean/blob/5cb725981b3ad137103ef908eb6ecff9e7ed9bdf/ErdosLean/Erdos1167.lean#L990.

Finite-target case. When all \(\kappa_\alpha\) are finite, \(\kappa_\alpha + 1\) is the ordinary natural-number successor. Special case of erdos_1167.

This case was proved by Erdős, Hajnal, Máté and Rado [EHMR84], using the Erdős–Rado tree argument and the negative stepping-up lemma. The statement omits the condition \(n_\alpha > r\). This is harmless, since a colouring that witnesses \(\lambda \not\to (n_\alpha)^r_{\alpha < \gamma}\) can only use colours \(\alpha\) with \(n_\alpha > r\).

theorem finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ
        (fun α => (n α : Cardinal.{u}) + 1) →
    cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u}))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1167.lean, line 82.

Erdos1167.erdos_1167.variants.binary_colors

Open: stated without proof.

Binary-color case. The \(\gamma = 2\) specialization (two color classes).

theorem binary_colors (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (κ : (2 : Ordinal.{u}).ToType → Cardinal.{u}) (hκ : ∀ α, (r : Cardinal.{u}) < κ α) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) 2 (fun α => κ α + 1) →
    cardinalPartitionRel lam r 2 κ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1167.lean, line 93.

Erdos1167.erdos_1167.variants.infinite_targets

Open: stated without proof.

Infinite-target case. When all \(\kappa_\alpha \geq \aleph_0\) are infinite and bounded by \(\lambda\), \(\kappa_\alpha + 1 = \kappa_\alpha\), so the hypothesis simplifies to a "pure" stepping-down lemma:

\[2^\lambda \to (\kappa_\alpha)_{\alpha\lt \gamma}^{r+1} \implies \lambda \to (\kappa_\alpha)_{\alpha\lt \gamma}^r.\]

The condition \(\kappa_\alpha \leq \lambda\) is needed to avoid a size obstruction: without it, the conclusion would require a subset of \(\lambda\) of size \(\kappa_\alpha > \lambda\), which is impossible (see infinite_targets_needs_bound).

theorem infinite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ i, ℵ₀ ≤ κ i)
    (hκ_le : ∀ i, κ i ≤ lam) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ →
    cardinalPartitionRel lam r γ κ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1167.lean, line 110.

Erdos1167.erdos_1167.variants.r_eq_two

Open: stated without proof.

\(r = 2\) case. The stepping-down from 3-uniform to 2-uniform partition relations: \(2^\lambda \to (\kappa_\alpha + 1)_{\alpha\lt \gamma}^3\) implies \(\lambda \to (\kappa_\alpha)_{\alpha\lt \gamma}^2\). Generalises the classical Erdős–Rado stepping-up/down theorem for pairs.

theorem r_eq_two (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam)
    (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u})
    (hκ : ∀ α, (2 : Cardinal.{u}) < κ α) :
    cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) 3 γ (fun α => κ α + 1) →
    cardinalPartitionRel lam 2 γ κ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1167.lean, line 124.

Sources

• FormalConjectures/ErdosProblems/1167.lean at 2055e5ad
• erdosproblems.com/1167

LeanErdos1167.erdos_1167 · Erdos1167.erdos_1167.variants.finite_targets · Erdos1167.erdos_1167.variants.binary_colors · Erdos1167.erdos_1167.variants.infinite_targets · Erdos1167.erdos_1167.variants.r_eq_two

TheoremErdős Problem 1168#

References: * erdosproblems.com/1168 * [EHR65] Erdős, P., Hajnal, A. and Rado, R., Partition relations for cardinal numbers. Acta Math. Acad. Sci. Hungar. (1965), pp. 93–196.

Quoted from FormalConjectures/ErdosProblems/1168.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1168.

The file states 2 research or textbook statements: 1 open and 1 solved. It also has 2 test statements, counted here but not shown.

Erdos1168.erdos_1168

Open: stated without proof.

Erdős Problem 1168. Prove that

\[\aleph_{\omega+1} \not\to (\aleph_{\omega+1}, \underbrace{3, 3, \ldots}_{\aleph_0})^2_{\aleph_0}\]

without assuming the generalized continuum hypothesis.

A problem of Erdős, Hajnal, and Rado [EHR65]: the negative arrow is known under GCH; the open problem asks for a ZFC proof. Here ω = Ordinal.omega0, so ℵ_ (ω + 1) is the successor cardinal of the singular ℵ_ω.

theorem erdos_1168 : ¬ CardinalCountableColorRamsey (ℵ_ (ω + 1))

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1168.lean, line 46.

Erdos1168.erdos_1168.variants.under_GCH

Solved: stated here without proof.

Erdős–Hajnal–Rado theorem under GCH [EHR65]: the negative partition relation \(\aleph_{\omega+1} \not\to (\aleph_{\omega+1}, 3, 3, \ldots)^2_{\aleph_0}\) holds assuming GCH.

theorem under_GCH (hGCH : GCH) : ¬ CardinalCountableColorRamsey (ℵ_ (ω + 1))

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1168.lean, line 57.

Sources

• FormalConjectures/ErdosProblems/1168.lean at 2055e5ad
• erdosproblems.com/1168

LeanErdos1168.erdos_1168 · Erdos1168.erdos_1168.variants.under_GCH

TheoremErdős Problem 1169#

Reference: erdosproblems.com/1169

References: - [Ha71] Hajnal, A. A negative partition relation. Proc. Nat. Acad. Sci. U.S.A. 68 (1971), pp. 142–144.

Quoted from FormalConjectures/ErdosProblems/1169.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1169.

The file states 3 research or textbook statements: 2 open and 1 solved. It also has 1 test statement, counted here but not shown.

Erdos1169.erdos_1169

Open: stated without proof.

Is it true that \(\omega_1^2 \not\to (\omega_1^2, 3)^2\)?

A problem of Erdős and Hajnal. Hajnal [Ha71] proved this assuming the continuum hypothesis. The source's displayed relation has blue target \(3\); its introductory \(k\) does not occur in that relation. See also erdosproblems.com/592.

theorem erdos_1169 :
    ¬ OrdinalRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) ^ (2 : ℕ)) (3 : Ordinal)

Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/1169.lean, line 50.

Erdos1169.erdos_1169.variants.finite_blue_target

Open: stated without proof.

The finite-blue-target form asks whether \(\omega_1^2 \not\to (\omega_1^2, k)^2\) for every \(k \ge 3\). The restriction excludes \(k \le 2\), where the positive relation holds. A colouring witnessing the negative relation with blue target \(3\) also witnesses this form.

theorem finite_blue_target :
    ∀ k : ℕ, 3 ≤ k →
      ¬ OrdinalRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) ^ (2 : ℕ)) (k : Ordinal)

Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/1169.lean, line 64.

Erdos1169.erdos_1169.variants.hajnal_under_ch

Solved: stated here without proof.

Hajnal (1971), assuming CH. Under the Continuum Hypothesis, \(\omega_1^2 \not\to (\omega_1^2, k)^2\) holds for every finite \(k \ge 3\).

theorem hajnal_under_ch (hCH : 𝔠 = ℵ_ 1) :
    ∀ k : ℕ, 3 ≤ k → ¬ OrdinalRamsey ((ω_ 1) ^ (2 : ℕ)) ((ω_ 1) ^ (2 : ℕ)) (k : Ordinal)

Category research solved; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/1169.lean, line 74.

Sources

• FormalConjectures/ErdosProblems/1169.lean at 2055e5ad
• erdosproblems.com/1169

LeanErdos1169.erdos_1169 · Erdos1169.erdos_1169.variants.finite_blue_target · Erdos1169.erdos_1169.variants.hajnal_under_ch

TheoremErdős Problem 1171#

Reference: erdosproblems.com/1171

Quoted from FormalConjectures/ErdosProblems/1171.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1171.

The file states 2 research or textbook statements: 1 open and 1 solved. It also has 1 API statement, counted here but not shown.

Erdos1171.erdos_1171

Open: stated without proof.

Erdős Problem 1171. Is it true that for all finite \(k < \omega\),

\[\omega_1^2 \to (\omega_1 \cdot \omega, \underbrace{3, \ldots, 3}_{k})^2_{k+1}?\]

In any \((k+1)\)-coloring of the pairs of the complete graph on \(\omega_1^2\), either there is a color-0 set of order type \(\omega_1 \cdot \omega\), or there is a monochromatic triangle \(K_3\) in some non-zero color. The case \(k = 1\) (erdos_1171.variants.k_one) is the Erdős–Hajnal theorem [EH74].

theorem erdos_1171 :
    ∀ k : ℕ, OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 k

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1171.lean, line 43.

Erdos1171.erdos_1171.variants.k_one

Solved: stated here without proof.

Erdős–Hajnal theorem [EH74]: the case \(k = 1\), \(\omega_1^2 \to (\omega_1 \cdot \omega, 3)^2\).

theorem k_one : OrdinalMultiColorRamsey (ω_ 1 ^ 2) (ω_ 1 * ω) 3 1

Category research solved; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1171.lean, line 54.

Sources

• FormalConjectures/ErdosProblems/1171.lean at 2055e5ad
• erdosproblems.com/1171

LeanErdos1171.erdos_1171 · Erdos1171.erdos_1171.variants.k_one

TheoremErdős Problem 1173#

Reference: erdosproblems.com/1173

Quoted from FormalConjectures/ErdosProblems/1173.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1173.

The file states 3 research or textbook statements: 1 open and 2 textbook results. It also has 4 test statements, counted here but not shown.

Erdos1173.erdos_1173

Open: stated without proof.

Erdős–Hajnal Problem 1173 [EH74]. Assume GCH. Let \(f : \omega_{\omega+1} \to [\omega_{\omega+1}]^{\leq \aleph_\omega}\) be a set mapping such that \(|f(\alpha) \cap f(\beta)| < \aleph_\omega\) for all \(\alpha \neq \beta\). Does there exist a free set of cardinality \(\aleph_{\omega+1}\)?

theorem erdos_1173 :
    GCH →
    ∀ f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType,
      IsSetMapping f →
      ∃ Y : Set (ω_ (ω + 1)).ToType, IsFreeSet f Y ∧ #Y = ℵ_ (ω + 1)

Category research open; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/1173.lean, line 55.

Erdos1173.erdos_1173.variants.free_set_mono

Textbook result, proved here.

Free sets are downward-closed under inclusion.

theorem erdos_1173.variants.free_set_mono
    (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType)
    {Y Z : Set (ω_ (ω + 1)).ToType}
    (hYZ : Z ⊆ Y) (hY : IsFreeSet f Y) : IsFreeSet f Z

Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/1173.lean, line 94.

Erdos1173.erdos_1173.variants.image_lt_aleph_succ

Textbook result, proved here.

Under IsSetMapping f, each image has cardinality < ℵ_{ω+1}.

theorem erdos_1173.variants.image_lt_aleph_succ
    (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType)
    (hf : IsSetMapping f)
    (α : (ω_ (ω + 1)).ToType) :
    #(f α) < ℵ_ (ω + 1)

Category textbook; AMS 03 Mathematical logic and foundations. Declared in FormalConjectures/ErdosProblems/1173.lean, line 103.

Sources

• FormalConjectures/ErdosProblems/1173.lean at 2055e5ad
• erdosproblems.com/1173

LeanErdos1173.erdos_1173 · Erdos1173.erdos_1173.variants.free_set_mono · Erdos1173.erdos_1173.variants.image_lt_aleph_succ

TheoremErdős Problem 1174#

References: - erdosproblems.com/1174 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999), problem 7.91.

Quoted from FormalConjectures/ErdosProblems/1174.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1174.

The file states 2 research or textbook statements: 2 open. It also has 2 test statements, counted here but not shown.

Erdos1174.erdos_1174.parts.i

Open: stated without proof.

Erdős Problem 1174, part (i) [Va99, 7.91]. A problem of Erdős and Hajnal: does there exist a graph \(G\) with no \(K_4\) such that every edge colouring of \(G\) with countably many colours contains a monochromatic \(K_3\)?

For simplicity the colourings are given on all unordered pairs \(\operatorname{Sym}_2(V)\); only the values on the edges of \(G\) matter, since a monochromatic triangle is witnessed by edges alone.

Shelah proved that a graph with this property can consistently exist, so the problem is not disprovable in ZFC; whether such a graph exists outright remains open.

theorem erdos_1174.parts.i :
    ∃ (V : Type) (G : SimpleGraph V), G.CliqueFree 4 ∧
      ∀ c : Sym2 V → ℕ, ∃ x y z : V,
        G.Adj x y ∧ G.Adj y z ∧ G.Adj x z ∧
        c s(x, y) = c s(y, z) ∧ c s(y, z) = c s(x, z)

Category research open; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1174.lean, line 50.

Erdos1174.erdos_1174.parts.ii

Open: stated without proof.

Erdős Problem 1174, part (ii) [Va99, 7.91]. A problem of Erdős and Hajnal: does there exist a graph \(G\) with no \(K_{\aleph_1}\) (that is, every clique of \(G\) is countable) such that every edge colouring of \(G\) with countably many colours contains a monochromatic \(K_{\aleph_0}\) (an infinite clique all of whose edges receive the same colour)?

For simplicity the colourings are given on all unordered pairs \(\operatorname{Sym}_2(V)\); only the values on the edges of \(G\) matter.

Shelah proved that a graph with this property can consistently exist, so the problem is not disprovable in ZFC; whether such a graph exists outright remains open.

theorem erdos_1174.parts.ii :
    ∃ (V : Type) (G : SimpleGraph V),
      (∀ S : Set V, G.IsClique S → #S ≤ ℵ₀) ∧
      ∀ c : Sym2 V → ℕ, ∃ S : Set V, G.IsClique S ∧ S.Infinite ∧
        ∃ k : ℕ, ∀ x ∈ S, ∀ y ∈ S, x ≠ y → c s(x, y) = k

Category research open; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1174.lean, line 71.

Sources

• FormalConjectures/ErdosProblems/1174.lean at 2055e5ad
• erdosproblems.com/1174

LeanErdos1174.erdos_1174.parts.i · Erdos1174.erdos_1174.parts.ii

TheoremErdős Problem 1175#

Reference: erdosproblems.com/1175

• [KoSh88] Komjáth, Péter and Shelah, Saharon, Forcing constructions for uncountably chromatic graphs. J. Symbolic Logic (1988), 696--707.

Formalization notes

• Chromatic cardinal: SimpleGraph.chromaticCardinal is the cardinal-valued chromatic number defined in FormalConjecturesForMathlib. It extends the finite chromaticNumber (which takes values in ℕ∞) to a Cardinal, and is therefore able to distinguish between different infinite chromatic numbers.
• Triangle-free subgraph: a subgraph H : G.Subgraph is triangle-free when H.coe.CliqueFree 3. This is the standard Mathlib formulation: CliqueFree 3 means the graph has no K₃ as a clique.
• Subgraph: we use G.Subgraph (an arbitrary subgraph record) rather than an induced subgraph since the problem asks for any subgraph, not just induced ones.

Quoted from FormalConjectures/ErdosProblems/1175.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1175.

The file states 3 research or textbook statements: 3 open. It also has 2 test statements, counted here but not shown.

Erdos1175.erdos_1175

Open: stated without proof.

Let \(\kappa\) be an uncountable cardinal. Must there exist a cardinal \(\lambda\) such that every graph with chromatic number \(\lambda\) contains a triangle-free subgraph with chromatic number \(\kappa\)?

Shelah proved that a negative answer is consistent when \(\kappa = \lambda = \aleph_1\) (see erdos_1175.variants.aleph_one).

theorem erdos_1175 :
    ∀ (κ : Cardinal), ℵ₀ < κ →
      ∃ (μ : Cardinal),
        ∀ (V : Type*) (G : SimpleGraph V), G.chromaticCardinal = μ →
          ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1175.lean, line 55.

Erdos1175.erdos_1175.variants.aleph_one

Open: stated without proof.

The case \(\kappa = \lambda = \aleph_1\) of Problem 1175: does every graph with chromatic number \(\aleph_1\) contain a triangle-free subgraph with chromatic number \(\aleph_1\)?

Shelah proved that a negative answer is consistent with ZFC [KoSh88, Theorem 1]: there is a model of ZFC containing a graph with chromatic number \(\aleph_1\) all of whose triangle-free subgraphs have countable chromatic number. Consistency results about models of ZFC are not directly formalizable inside Lean's fixed model, so only the underlying question is recorded here. Note that this concerns only the choice \(\lambda = \aleph_1\); it does not rule out a larger \(\lambda\) in erdos_1175.

theorem erdos_1175.variants.aleph_one :
    ∀ (V : Type*) (G : SimpleGraph V), G.chromaticCardinal = ℵ_ 1 →
      ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = ℵ_ 1

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1175.lean, line 74.

Erdos1175.erdos_1175.variants.threshold_formulation

Open: stated without proof.

Threshold reformulation variant. Replaces chromaticCardinal = λ in the hypothesis of erdos_1175 with λ ≤ chromaticCardinal (a graph of chromatic number ≥ λ has a triangle-free subgraph of chromatic number κ). This is a strengthening of erdos_1175 (see erdos_1175.test.threshold_implies_exact).

theorem erdos_1175.variants.threshold_formulation :
    ∀ (κ : Cardinal), ℵ₀ < κ →
      ∃ (μ : Cardinal),
        ∀ (V : Type*) (G : SimpleGraph V), μ ≤ G.chromaticCardinal →
          ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1175.lean, line 86.

Sources

• FormalConjectures/ErdosProblems/1175.lean at 2055e5ad
• erdosproblems.com/1175

LeanErdos1175.erdos_1175 · Erdos1175.erdos_1175.variants.aleph_one · Erdos1175.erdos_1175.variants.threshold_formulation

TheoremErdős Problem 1176#

Reference: erdosproblems.com/1176

Quoted from FormalConjectures/ErdosProblems/1176.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1176.

The file states 1 research or textbook statement: 1 open.

Erdos1176.erdos_1176

Open: stated without proof.

Let \(G\) be a graph with chromatic number \(\aleph_1\). Is it true that there is a colouring of the edges with \(\aleph_1\) many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?

A problem of Erdős, Galvin, and Hajnal. The consistency of this was proved by Hajnal and Komjáth.

theorem erdos_1176 :
    ∀ {V : Type*} (G : SimpleGraph V), G.chromaticCardinal = aleph 1 →
      ∃ (EColor : Type) (_ : mk EColor = aleph 1) (c_edge : G.edgeSet → EColor),
        ∀ (VColor : Type) (_ : mk VColor ≤ aleph 0) (c_vert : V → VColor),
          ∃ (vc : VColor),
            ∀ (ec : EColor), ∃ (u v : V) (h : G.Adj u v),
              c_vert u = vc ∧ c_vert v = vc ∧ c_edge ⟨s(u, v), h⟩ = ec

Category research open; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1176.lean, line 40.

Sources

• FormalConjectures/ErdosProblems/1176.lean at 2055e5ad
• erdosproblems.com/1176

LeanErdos1176.erdos_1176

TheoremErdős Problem 1177#

References: - erdosproblems.com/1177 - [Li26] Li, E., A Resolution of Erdős Problems 593 and 1177: Obligatory Triple Systems and Exact Spectra. arXiv:2606.24882v2 (2026), Corollary 1.4.

Quoted from FormalConjectures/ErdosProblems/1177.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1177.

The file states 3 research or textbook statements: 3 solved.

Erdos1177.erdos_1177.parts.i

Solved: stated here without proof.

Let \(G\) be a finite \(3\)-uniform hypergraph, and let \(F_G(\kappa)\) denote the collection of \(3\)-uniform hypergraphs with chromatic number \(\kappa\) not containing \(G\). If \(F_G(\aleph_1)\) is non-empty, then it contains a hypergraph on at most \(2^{2^{\aleph_0}}\) vertices. Li [Li26, Corollary 1.4(1)] proved this.

theorem erdos_1177.parts.i :
    ∀ (W : Type) [Fintype W] (G : UniformHypergraph W 3),
    G.HasAvoidingChromaticCardinal ℵ₁ →
      ∃ (V : Type) (_ : DecidableEq V) (X : UniformHypergraph V 3),
        X.chromaticCardinal = ℵ₁ ∧ ¬ G.Appears X ∧
          Cardinal.mk V ≤ (2 : Cardinal) ^ ((2 : Cardinal) ^ ℵ₀)

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1177.lean, line 43.

Erdos1177.erdos_1177.parts.ii

Solved: stated here without proof.

The assertion that two non-empty avoidance families \(F_G(\aleph_1)\) and \(F_H(\aleph_1)\) always have non-empty intersection is false. Li [Li26, Corollary 1.4(2)] gives a counterexample using two triples sharing a pair and the loose seven-cycle.

theorem erdos_1177.parts.ii :
    ¬ ∀ (W U : Type) [Fintype W] [Fintype U]
    (G : UniformHypergraph W 3) (H : UniformHypergraph U 3),
    G.HasAvoidingChromaticCardinal ℵ₁ → H.HasAvoidingChromaticCardinal ℵ₁ →
      ∃ (V : Type) (_ : DecidableEq V) (X : UniformHypergraph V 3),
        X.chromaticCardinal = ℵ₁ ∧ ¬ G.Appears X ∧ ¬ H.Appears X

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1177.lean, line 57.

Erdos1177.erdos_1177.parts.iii

Solved: stated here without proof.

If \(\kappa,\lambda\) are uncountable cardinals and \(F_G(\kappa)\) is non-empty then \(F_G(\lambda)\) is non-empty. Li [Li26, Corollary 1.4(3)] proved this.

theorem erdos_1177.parts.iii :
    ∀ (W : Type) [Fintype W] (G : UniformHypergraph W 3)
    (κ μ : Cardinal), ℵ₀ < κ → ℵ₀ < μ →
      G.HasAvoidingChromaticCardinal κ → G.HasAvoidingChromaticCardinal μ

Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1177.lean, line 70.

Sources

• FormalConjectures/ErdosProblems/1177.lean at 2055e5ad
• erdosproblems.com/1177

LeanErdos1177.erdos_1177.parts.i · Erdos1177.erdos_1177.parts.ii · Erdos1177.erdos_1177.parts.iii

TheoremErdős Problem 1178#

References: - erdosproblems.com/1178 - [BES73] Brown, W. G. and Erdős, P. and S\'os, V. T., Some extremal problems on {\(r\)}-graphs. (1973), 53--63. - [CGLS23] Conlon, David and Gishboliner, Lior and Levanzov, Yevgeny and Shapira, Asaf, A new bound for the {B}rown-{E}rd\H os-S\'os problem. J. Combin. Theory Ser. B (2023), 1--35. - [EFR86] Erdős, P. and Frankl, P. and Rödl, V., The asymptotic number of graphs not containing a fixed subgraph and a problem for hypergraphs having no exponent. Graphs Combin. (1986), 113-121. - [Er75b] Erdős, Paul, Problems and results in combinatorial number theory. Journ\'{e}es Arithm\'{e}tiques de Bordeaux (Conf., Univ. Bordeaux, Bordeaux, 1974) (1975), 295-310. - [RuSz78] Ruzsa, I. Z. and Szemer\'{e}di, E., Triple systems with no six points carrying three triangles. Combinatorics (Proc. Fifth Hungarian Colloq., Keszthely, 1976), Vol. II (1978), 939-945. - [SaSe05] Sárk\"ozy, Gábor N. and Selkow, Stanley, An extension of the {R}uzsa-Szemer\'edi theorem . Combinatorica (2005), 77--84. - [SoSo17] Solymosi, David and Solymosi, Jozsef, Small cores in 3-uniform hypergraphs. J. Combin. Theory Ser. B (2017), 897--910.

Quoted from FormalConjectures/ErdosProblems/1178.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1178.

The file states 1 research or textbook statement: 1 open.

Erdos1178.erdos_1178

Open: stated without proof.

For \(r\geq 3\) let \(d_r(e)\) be the minimal \(d\) such that

\[\mathrm{ex}_r(n,\mathcal{F})=o(n^2),\]

where \(\mathcal{F}\) is the family of \(r\)-uniform hypergraphs on \(d\) vertices with \(e\) edges. Prove that

\[d_r(e)=(r-2)e+3\]

for all \(r,e\geq 3\).

theorem erdos_1178 :
    ∀ r e : ℕ, 3 ≤ r → 3 ≤ e →
    Hypergraph.sparseConfigurationThreshold r e = (((r - 2) * e + 3 : ℕ) : ℕ∞)

Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1178.lean, line 56.

Sources

• FormalConjectures/ErdosProblems/1178.lean at 2055e5ad
• erdosproblems.com/1178

LeanErdos1178.erdos_1178

TheoremErdős Problem 1179#

References: - erdosproblems.com/1179 - [Er73] Erdős, P., Problems and results on combinatorial number theory. A survey of combinatorial theory (Proc. Internat. Sympos., Colorado State Univ., Fort Collins, Colo., 1971) (1973), 117-138. - [ErRe65] Erdős, P. and Rényi, A., Probabilistic methods in group theory. J. Analyse Math. (1965), 127-138. - [ErHa76] Erdős, P. and Hall, R. R., Probabilistic methods in group theory. II. Houston J. Math. (1976), 173-180.

Quoted from FormalConjectures/ErdosProblems/1179.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1179.

The file states 2 research or textbook statements: 2 solved.

Erdos1179.erdos_1179

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1179.lean#L3564.

Let \(0\lt \epsilon<1\) and let \(g_\epsilon(N)\) be the minimal \(k\) such that if \(G\) is an abelian group of size \(N\) and \(A\subseteq G\) is a uniformly random subset of size \(k\), and

\[F_A(g) = \#\left\{ S\subseteq A : g = \sum_{x\in S}x\right\},\]

then, with probability \(\to 1\) as \(N\to \infty\),

\[\left\lvert F_A(g)-\frac{2^k}{N}\right\rvert \leq \epsilon \frac{2^k}{N}\]

for all \(g\in G\).

Estimate \(g_\epsilon(N)\) - in particular, is it true that for all \(\epsilon>0\)

\[g_\epsilon(N)=(1+o_\epsilon(1))\log_2N?\]

It is trivial that \(g_\epsilon(N)\geq \log_2N\) for all \(0\lt \epsilon<1\). Erdős and Rényi [ErRe65] proved that for all \(0\lt \epsilon<1\), \(g_\epsilon(N) \leq (2+o(1))\log_2N+O_\epsilon(1)\). Erdős and Hall [ErHa76] proved that, for all \(0\lt \epsilon<1\),

\[g_\epsilon(N)\leq \left(1+O_\epsilon\left(\frac{\log\log\log N}{\log\log N}\right)\right) \log_2N.\]

The upper bound \(g_\epsilon(N)\leq (1+o(1))\log_2 N\) is formalised as: there is a choice of sizes \(k(N) = (1+o(1))\log_2 N\) such that, along any sequence of abelian groups with \(|G|\to\infty\), the probability that a random \(k(|G|)\)-subset is \(\epsilon\)-balanced tends to \(1\). The matching lower bound is erdos_1179.variants.lower_bound.

See also 543.

theorem erdos_1179 : ∀ ε : ℝ, 0 < ε → ε < 1 → ∃ k : ℕ → ℕ,
    Tendsto (fun N : ℕ ↦ (k N : ℝ) / Real.logb 2 N) atTop (nhds 1) ∧
      ∀ (G : ℕ → Type) [∀ i, AddCommGroup (G i)] [∀ i, Fintype (G i)],
        Tendsto (fun i ↦ Fintype.card (G i)) atTop atTop →
          Tendsto (fun i ↦ successProbability (G i) ε (k (Fintype.card (G i)))) atTop
            (nhds 1)

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1179.lean, line 86.

Erdos1179.erdos_1179.variants.lower_bound

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1179.lean#L3564.

It is trivial that \(g_\epsilon(N)\geq \log_2N\): an \(\epsilon\)-balanced set \(A\) with \(\epsilon < 1\) must satisfy \(|G| \leq 2^{|A|}\), since every \(g\) has a representation.

theorem erdos_1179.variants.lower_bound : ∀ ε : ℝ, 0 < ε → ε < 1 →
    ∀ A : Finset G, IsBalanced ε A → Fintype.card G ≤ 2 ^ A.card

Category research solved; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1179.lean, line 99.

Sources

• FormalConjectures/ErdosProblems/1179.lean at 2055e5ad
• erdosproblems.com/1179

LeanErdos1179.erdos_1179 · Erdos1179.erdos_1179.variants.lower_bound

TheoremErdős Problem 1180#

References: - erdosproblems.com/1180 - [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980). - [Sh02] Shparlinski, Igor E., On a question of Erdős and Graham. Arch. Math. (Basel) (2002), 445-448. - [Gl06] Glibichuk, A. A., Combinatorial properties of sets of residues modulo a prime and the Erdős-Graham problem. Mat. Zametki (2006), 384-395. - PALOMAR-2026-10-12-000005

Quoted from FormalConjectures/ErdosProblems/1180.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The problem's page on erdosproblems.com: https://www.erdosproblems.com/1180.

The file states 5 research or textbook statements: 1 open and 4 solved.

Erdos1180.erdos_1180

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1180.lean#L1249.

Let \(\epsilon>0\). Does there exist a constant \(C_\epsilon\) such that, for all primes \(p\), every residue modulo \(p\) is the sum of at most \(C_\epsilon\) many elements of

\[\{ n^{-1} : 1\leq n\leq p^\epsilon\}\]

where \(n^{-1}\) denotes the inverse of \(n\) modulo \(p\)?

The original question was answered in the affirmative by Shparlinski [Sh02], who proved that \(\ll \epsilon^{-3}\) summands suffice for all sufficiently large primes. This was improved to \(\ll \epsilon^{-2}\) by Glibichuk [Gl06]. It is trivial that at least \(\gg \epsilon^{-1}\) summands are required, and it may be that \(C_\epsilon\leq \epsilon^{-1-o(1)}\) is possible.

See also 540.

theorem erdos_1180 : ∀ ε : ℝ, 0 < ε → ∃ C : ℕ, ∀ p : ℕ, p.Prime → ∀ a : ZMod p,
    ∃ s : Multiset ℕ, s.card ≤ C ∧ Represents ε p a s

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1180.lean, line 71.

Erdos1180.erdos_1180.variants.shparlinski

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/ba96303b34a95ac458958c1eb0bbdee54733484a/erdos-1180/Solution.lean#L89.

Shparlinski [Sh02] proved that \(\ll \epsilon^{-3}\) summands suffice for every residue modulo every sufficiently large prime, where the threshold on \(p\) may depend on \(\epsilon\). No bound polynomial in \(\epsilon^{-1}\) can hold for all primes, since when \(p^\epsilon < 2\) the only admissible denominator is \(1\).

theorem erdos_1180.variants.shparlinski : ∃ K : ℝ, ∀ ε : ℝ, 0 < ε → ε ≤ 1 →
    ∃ P : ℕ, ∀ p : ℕ, P ≤ p → p.Prime → ∀ a : ZMod p,
      ∃ s : Multiset ℕ, (s.card : ℝ) ≤ K * ε⁻¹ ^ 3 ∧ Represents ε p a s

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1180.lean, line 84.

Erdos1180.erdos_1180.variants.glibichuk

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/ba96303b34a95ac458958c1eb0bbdee54733484a/erdos-1180/Solution.lean#L83.

Glibichuk [Gl06] improved the bound to \(\ll \epsilon^{-2}\) summands, again for every sufficiently large prime.

theorem erdos_1180.variants.glibichuk : ∃ K : ℝ, ∀ ε : ℝ, 0 < ε → ε ≤ 1 →
    ∃ P : ℕ, ∀ p : ℕ, P ≤ p → p.Prime → ∀ a : ZMod p,
      ∃ s : Multiset ℕ, (s.card : ℝ) ≤ K * ε⁻¹ ^ 2 ∧ Represents ε p a s

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1180.lean, line 96.

Erdos1180.erdos_1180.variants.lower_bound

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/ba96303b34a95ac458958c1eb0bbdee54733484a/erdos-1180/Solution.lean#L95.

It is trivial that at least \(\gg \epsilon^{-1}\) summands are required.

theorem erdos_1180.variants.lower_bound : ∃ K : ℝ, 0 < K ∧ ∀ ε : ℝ, 0 < ε → ε ≤ 1 →
    K * ε⁻¹ ≤ C ε

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1180.lean, line 105.

Erdos1180.erdos_1180.variants.optimal

Open: stated without proof.

Is \(C_\epsilon\leq \epsilon^{-1-o(1)}\)? Here \(C_\epsilon\) is the number of summands needed for every sufficiently large prime, as in erdos_1180.variants.shparlinski and erdos_1180.variants.glibichuk. For all primes no such bound holds, since when \(p^\epsilon < 2\) the only admissible denominator is \(1\).

theorem erdos_1180.variants.optimal : ∀ δ : ℝ, 0 < δ →
    ∀ᶠ ε : ℝ in nhdsWithin 0 (Set.Ioi 0), ∃ P : ℕ, ∀ p : ℕ, P ≤ p → p.Prime → ∀ a : ZMod p,
      ∃ s : Multiset ℕ, (s.card : ℝ) ≤ ε⁻¹ ^ (1 + δ) ∧ Represents ε p a s

Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1180.lean, line 116.

Sources

• FormalConjectures/ErdosProblems/1180.lean at 2055e5ad
• erdosproblems.com/1180

LeanErdos1180.erdos_1180 · Erdos1180.erdos_1180.variants.shparlinski · Erdos1180.erdos_1180.variants.glibichuk · Erdos1180.erdos_1180.variants.lower_bound · Erdos1180.erdos_1180.variants.optimal

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.