Erdős Problem 1100 to Erdős Problem 1126

TheoremErdős Problem 1100#

References: - erdosproblems.com/1100 - [ErHa78] Erdős, P. and Hall, R. R., On some unconventional problems on the divisors of integers. J. Austral. Math. Soc. Ser. A 25 (1978), 479-485. PDF - [Er81h] Erdős, P., Some problems and results on additive and multiplicative number theory. Analytic number theory (Philadelphia, Pa., 1980) (1981), 171-182. PDF - [ErTe89] Erdős, P. and Tenenbaum, G., Sur les fonctions arithmétiques liées aux diviseurs consécutifs. J. Number Theory 31 (1989), 285-311. PDF

The function \(\tau_\perp(n)\) is called \(\tau_r(n)\) in [Er81h] and \(f(n)\) in [ErHa78] and [ErTe89].

Quoted from FormalConjectures/ErdosProblems/1100.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/1100.

The file states 10 research or textbook statements: 1 open, 8 solved and 1 textbook result.

Erdos1100.erdos_1100.parts.i

Solved: stated here without proof.

If \(1=d_1\lt \cdots\lt d_{\tau(n)}=n\) are the divisors of \(n\), then let \(\tau_\perp(n)\) count the number of \(i\) for which \((d_i,d_{i+1})=1\).

Is it true that \(\tau_\perp(n)/\omega(n)\to \infty\) for almost all \(n\)?

This is the first part, asked by Erdős and Hall [ErHa78, p. 483]. We read it as: for every \(C\) the set of \(n\) with \(\tau_\perp(n)\leq C\omega(n)\) has natural density \(0\). This is equivalent to \(\tau_\perp(n)/\omega(n)\to\infty\) along a set of density \(1\), and it avoids dividing by \(\omega(1)=0\).

The answer is yes. By [ErTe89, Corollary 2, p. 288], \(\tau_\perp(n)\geq(\log n)^{\log 3-1+o(1)}\) for almost all \(n\) (see erdos_1100.variants.normal_order), while \(\omega(n)\sim\log\log n\) for almost all \(n\) (Hardy-Ramanujan).

theorem erdos_1100.parts.i :
    ∀ C : ℝ, {n : ℕ | (tauPerp n : ℝ) ≤ C * (ω n : ℝ)}.HasDensity 0

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

Erdos1100.erdos_1100.parts.ii

Solved: stated here without proof.

If \(1=d_1\lt \cdots\lt d_{\tau(n)}=n\) are the divisors of \(n\), then let \(\tau_\perp(n)\) count the number of \(i\) for which \((d_i,d_{i+1})=1\).

Is it true that

\[\tau_\perp(n)< \exp((\log n)^{o(1)})\]

for all \(n\)?

This is the second part. Erdős and Hall [ErHa78, p. 483] say it would be reasonable to expect that for every \(\epsilon>0\) one has \(\tau_\perp(n)\lt \exp((\log n)^{\epsilon})\); the problem page asks it as a question. We read \(o(1)\) as: for every \(\epsilon>0\) and all sufficiently large \(n\). This is equivalent to a bound for all \(n\) with an exponent that tends to \(0\). A bound for all \(n\) with a fixed small \(\epsilon\) fails: for example \(\tau_\perp(30)=4>\exp((\log 30)^{0.1})\).

The answer is no. Erdős and Tenenbaum [ErTe89, Theorem 4, p. 289] proved \(\max_{n\leq x}\tau_\perp(n)\geq\exp\bigl(((\log 2)^2+o(1))\log x/(\log\log x)^2\bigr)\) (see erdos_1100.variants.erdos_tenenbaum_max). This gives infinitely many \(n\) with \(\tau_\perp(n)>\exp((\log n)^{1/2})\).

theorem erdos_1100.parts.ii :
    ¬ ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (tauPerp n : ℝ) < Real.exp (Real.log n ^ ε)

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

Erdos1100.erdos_1100.parts.iii

Open: stated without proof.

Let

\[g(k) = \max_{\omega(n)=k}\tau_\perp(n),\]

where \(\omega(n)\) counts the number of distinct prime divisors of \(n\), and \(n\) is restricted to squarefree integers. Determine the growth of \(g(k)\).

This is the third part. We read "determine the growth" as \(g(k)=\Theta(\texttt{answer}\ k)\). Known bounds are \((\sqrt2+o(1))^k\lt g(k)<(2-c)^k\) [Er81h, p. 173] (see erdos_1100.variants.erdos_simonovits), and \(g(k)\leq 3\cdot(3\cdot 2^{-2/3})^k\) [ErTe89, Theorem 1] (see erdos_1100.variants.erdos_tenenbaum_g). So \(g\) is at most exponential, the lower bound announced in [Er81h] would make it exponential, and already the base of the exponential is open.

theorem erdos_1100.parts.iii :
    (fun k : ℕ ↦ (g k : ℝ)) =Θ[atTop] erdos_1100.parts.iii.answer

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

Erdos1100.erdos_1100.variants.omega_le

Textbook result, stated without proof.

It is trivial that \(\tau_\perp(n)\geq \omega(n)\) [ErHa78, p. 480], [ErTe89, (1.9), p. 288]: each prime divisor of \(n\) is the larger member of a coprime pair of consecutive divisors.

theorem erdos_1100.variants.omega_le : ∀ n : ℕ, 0 < n → ω n ≤ tauPerp n

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1100.lean, line 128.

Erdos1100.erdos_1100.variants.eq_omega

Solved: stated here without proof.

There is equality \(\tau_\perp(n)=\omega(n)\) for infinitely many \(n\): Erdős and Hall [ErHa78, p. 480] note equality when \(n=p_1\cdots p_k\) and \(p_i>p_1\cdots p_{i-1}\) for \(2\leq i\leq k\). Such \(n\) exist for every \(k\), which we state.

theorem erdos_1100.variants.eq_omega (k : ℕ) :
    ∃ n : ℕ, Squarefree n ∧ ω n = k ∧ tauPerp n = k

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

Erdos1100.erdos_1100.variants.erdos_hall

Solved: stated here without proof.

Erdős and Hall [ErHa78, Theorem 1, p. 480] prove, for all \(\epsilon>0\) and sufficiently large \(x\),

\[\max_{n\lt x} \tau_\perp(n) > \exp((\log\log x)^{2-\epsilon}).\]

We write the maximum as: some \(n\lt x\) has \(\tau_\perp(n)\) above the bound.

theorem erdos_1100.variants.erdos_hall : ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
    ∃ n : ℕ, (n : ℝ) < x ∧ Real.exp (Real.log (Real.log x) ^ (2 - ε)) < (tauPerp n : ℝ)

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

Erdos1100.erdos_1100.variants.erdos_tenenbaum_max

Solved: stated here without proof.

Erdős and Tenenbaum [ErTe89, Theorem 4, p. 289] improved this considerably: for \(x\geq 3\),

\[\max_{n\leq x}\tau_\perp(n)\geq \exp\Bigl(\bigl((\log 2)^2+o(1)\bigr) \frac{\log x}{(\log\log x)^2}\Bigr).\]

We write \(o(1)\) as an arbitrarily small \(\delta>0\) and the maximum as: some \(n\leq x\) has \(\tau_\perp(n)\) above the bound.

theorem erdos_1100.variants.erdos_tenenbaum_max : ∀ δ : ℝ, 0 < δ → ∀ᶠ x : ℝ in atTop,
    ∃ n : ℕ, (n : ℝ) ≤ x ∧
      Real.exp (((Real.log 2) ^ 2 - δ) * Real.log x / (Real.log (Real.log x)) ^ 2) ≤
        (tauPerp n : ℝ)

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

Erdos1100.erdos_1100.variants.normal_order

Solved: stated here without proof.

Erdős and Tenenbaum [ErTe89, Corollary 2, p. 288] proved that for almost all \(n\) (that is, on a set of density \(1\))

\[(\log n)^{\log 3-1+o(1)}\leq \tau_\perp(n)\leq (\log n)^{\log 2-1/2+o(1)}.\]

The paper credits the upper bound to an earlier work of the same authors (Bull. Soc. Math. France 111 (1983)). We write \(o(1)\) as: for every \(\epsilon>0\) the set of \(n\) with both bounds, with exponents shifted by \(\mp\epsilon\), has density \(1\).

theorem erdos_1100.variants.normal_order : ∀ ε : ℝ, 0 < ε →
    {n : ℕ | Real.log n ^ (Real.log 3 - 1 - ε) ≤ (tauPerp n : ℝ) ∧
      (tauPerp n : ℝ) ≤ Real.log n ^ (Real.log 2 - 1 / 2 + ε)}.HasDensity 1

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

Erdos1100.erdos_1100.variants.erdos_simonovits

Solved: stated here without proof.

Erdős and Simonovits (see [Er81h, p. 173]) proved

\[(2^{1/2}+o(1))^k < g(k) < (2-c)^k\]

for some constant \(c>0\). We write the lower bound as: every fixed \(0\leq r\lt \sqrt2\) satisfies \(r^k\lt g(k)\) for all large \(k\), and the upper bound for all large \(k\).

[Er81h] announces this without proof, and [ErTe89, p. 291] calls the argument of Erdős and Simonovits for squarefree \(n\), which it uses for the upper bound, unpublished. The upper bound also follows from erdos_1100.variants.erdos_tenenbaum_g.

theorem erdos_1100.variants.erdos_simonovits :
    (∀ r : ℝ, 0 ≤ r → r < Real.sqrt 2 → ∀ᶠ k : ℕ in atTop, r ^ k < (g k : ℝ)) ∧
      ∃ c : ℝ, 0 < c ∧ ∀ᶠ k : ℕ in atTop, (g k : ℝ) < (2 - c) ^ k

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

Erdos1100.erdos_1100.variants.erdos_tenenbaum_g

Solved: stated here without proof.

For squarefree \(n\) with \(\omega(n)=k\) the bound \(f(n)\leq 3\tau(n)B_1^{\omega_1(n)}\) of [ErTe89, Theorem 1, (1.3), p. 287], with \(B_1=3\cdot 2^{-5/3}\), gives

\[g(k)\leq 3\left(3\cdot 2^{-2/3}\right)^k,\]

and \(3\cdot 2^{-2/3}=1.88988\ldots<2\).

theorem erdos_1100.variants.erdos_tenenbaum_g (k : ℕ) :
    (g k : ℝ) ≤ 3 * (3 / (2 : ℝ) ^ ((2 : ℝ) / 3)) ^ k

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

Sources

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

LeanErdos1100.erdos_1100.parts.i · Erdos1100.erdos_1100.parts.ii · Erdos1100.erdos_1100.parts.iii · Erdos1100.erdos_1100.variants.omega_le · Erdos1100.erdos_1100.variants.eq_omega · Erdos1100.erdos_1100.variants.erdos_hall · Erdos1100.erdos_1100.variants.erdos_tenenbaum_max · Erdos1100.erdos_1100.variants.normal_order · Erdos1100.erdos_1100.variants.erdos_simonovits · Erdos1100.erdos_1100.variants.erdos_tenenbaum_g

TheoremErdős Problem 1101#

Reference: erdosproblems.com/1101

Quoted from FormalConjectures/ErdosProblems/1101.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/1101.

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

Erdos1101.erdos_1101.parts.i

Open: stated without proof.

1. There is NO good sequence with polynomial growth.

theorem erdos_1101.parts.i :
    ¬ ∃ u, IsGood u ∧ ∃ k : ℕ, (fun n => (u n : ℝ)) =O[atTop] (fun n => (n : ℝ) ^ k)

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

Erdos1101.erdos_1101.parts.ii

Open: stated without proof.

1. There is a good sequence with sub-exponential growth.

theorem erdos_1101.parts.ii :
    ∃ u, IsGood u ∧ (fun n => Real.log (u n : ℝ)) =o[atTop] (fun n => (n : ℝ))

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

Sources

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

LeanErdos1101.erdos_1101.parts.i · Erdos1101.erdos_1101.parts.ii

TheoremErdős Problem 1102#

Reference: erdosproblems.com/1102

Quoted from FormalConjectures/ErdosProblems/1102.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/1102.

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

Erdos1102.erdos_1102.density_zero_of_P

Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/1e075c4f6e8a907b924647fa88238f978e941742/ErdosProblem1102PropertyP.lean.

If A = {a₁ < a₂ < …} has property P, then A has natural density 0. Equivalently, (a_j / j) → ∞ as j → ∞. -

theorem erdos_1102.density_zero_of_P
    (A : ℕ → ℕ)
    (h_inc : StrictMono A)
    (hP : HasPropertyP (range A)) :
    Tendsto (fun j => (A j / j : ℝ)) atTop atTop

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

Erdos1102.erdos_1102.exists_sequence_with_P

Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/1e075c4f6e8a907b924647fa88238f978e941742/ErdosProblem1102PropertyP.lean.

Conversely, for any function f : ℕ → ℕ that goes to infinity, there exists a strictly increasing sequence A = {a₁ < a₂ < …} with property P such that (a_j / j) ≤ f(j) for all j. -

theorem erdos_1102.exists_sequence_with_P
    (f : ℕ → ℕ) (h_inf : Tendsto f atTop atTop)
    (h_pos : ∀ n, f n ≠ 0) :
    ∃ A : ℕ → ℕ, StrictMono A ∧
    HasPropertyP (range A) ∧
    ∀ j : ℕ, (A j : ℝ) / j ≤ f j

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

Erdos1102.erdos_1102.upper_density_Q

Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/1e075c4f6e8a907b924647fa88238f978e941742/ErdosProblem1102PropertyQDensity.lean.

Every sequence with property Q has upper density at most 6 / π^2.

theorem erdos_1102.upper_density_Q
    (A : ℕ → ℕ) (h_inc : StrictMono A)
    (hQ : HasPropertyQ (range A)) :
    limsup (fun j : ℕ  ↦ (j / A j : ℝ)) atTop ≤ 6 / Real.pi^2

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

Erdos1102.erdos_1102.lower_density_Q_exists

Solved: stated here; a Lean proof is at https://github.com/Woett/Lean-files/blob/1e075c4f6e8a907b924647fa88238f978e941742/ErdosProblem1102PropertyQDensity.lean.

There exists an infinite sequence \(A = {a₁ < a₂ < …} ⊂ \mathsf{SF}\) where \(\mathsf{SF} := \mathbb{N} \setminus \bigcup_{p} p^{2}\mathbb{N}\), i.e. the set of squarefree numbers. The set A has property Q and natural density 6 / π^2. Equivalently, (j / a_j) → 6/π^2 as j → ∞. -

theorem erdos_1102.lower_density_Q_exists :
    ∃ A : ℕ → ℕ, StrictMono A ∧
    (∀ j, Squarefree (A j)) ∧
    HasPropertyQ (range A) ∧
    Tendsto (fun j : ℕ  ↦ (j / A j : ℝ)) atTop (𝓝 (6 / Real.pi^2))

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

Sources

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

LeanErdos1102.erdos_1102.density_zero_of_P · Erdos1102.erdos_1102.exists_sequence_with_P · Erdos1102.erdos_1102.upper_density_Q · Erdos1102.erdos_1102.lower_density_Q_exists

TheoremErdős Problem 1104#

Reference: https://www.erdosproblems.com/1104

Quoted from FormalConjectures/ErdosProblems/1104.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/1104.

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

Erdos1104.erdos_1104.variants.lower

Solved: stated here without proof.

Lower bound (Hefty–Horn–King–Pfender 2025).

\[ (1 - o(1)) \sqrt{\frac{n}{\log n}} \le f(n), \]

where \(f(n)\) denotes the maximum chromatic number of a triangle-free graph on \(n\) vertices, formalized as triangleFreeMaxChromatic n.

theorem erdos_1104.variants.lower :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (1 - ε) * Real.sqrt (n : ℝ) / Real.sqrt (Real.log (n : ℝ))
        ≤ (triangleFreeMaxChromatic n : ℝ)

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

Erdos1104.erdos_1104.variants.upper

Solved: stated here without proof.

Upper bound (Davies–Illingworth 2022).

\[ f(n) \le (2 + o(1)) \sqrt{\frac{n}{\log n}}, \]

where \(f(n)\) denotes the maximum chromatic number of a triangle-free graph on \(n\) vertices, formalized as triangleFreeMaxChromatic n.

theorem erdos_1104.variants.upper :
    ∀ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
      (triangleFreeMaxChromatic n : ℝ)
        ≤ (2 + ε) * Real.sqrt (n : ℝ) / Real.sqrt (Real.log (n : ℝ))

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

Sources

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

LeanErdos1104.erdos_1104.variants.lower · Erdos1104.erdos_1104.variants.upper

TheoremErdős Problem 1105#

References: - erdosproblems.com/1105 - PALOMAR-2026-10-13-000006 - [ESS75] Erdős, P. and Simonovits, M. and Sós, V. T., Anti-{R}amsey theorems. (1975), 633--643. - [MoNe05] Montellano-Ballesteros, J. J. and Neumann-Lara, V., An anti-{R}amsey theorem on cycles. Graphs Combin. (2005), 343--354. - [SiSo84] Simonovits, Miklós and Sós, Vera T., On restricted colourings of {\(K_n\)}. Combinatorica (1984), 101--110. - [Yu21] L.-T. Yuan, The anti-Ramsey number for paths. arXiv:2102.00807 (2021).

Quoted from FormalConjectures/ErdosProblems/1105.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/1105.

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

Erdos1105.erdos_1105.parts.i

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

The anti-Ramsey number \(\mathrm{AR}(n,G)\) is the maximum possible number of colours in which the edges of \(K_n\) can be coloured without creating a rainbow copy of \(G\) (i.e. one in which all edges have different colours).

Let \(C_k\) be the cycle on \(k\) vertices. Is it true that \(\mathrm{AR}(n,C_k)=\left(\frac{k-2}{2}+\frac{1}{k-1}\right)n+O(1)\)?

Montellano-Ballesteros and Neumann-Lara [MoNe05] gave an exact formula for \(\mathrm{AR}(n,C_k)\), which implies in particular that \(\mathrm{AR}(n,C_k)=\left(\frac{k-2}{2}+\frac{1}{k-1}\right)n+O(1).\)

theorem erdos_1105.parts.i :
    ∀ k, 3 ≤ k →
    ((fun n => (antiRamseyNum (cycleGraph k) n : ℝ) - ((k - 2 : ℝ) / 2 + 1 / (k - 1)) * n)
      =O[atTop] (fun _ => (1 : ℝ)))

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

Erdos1105.erdos_1105.parts.ii

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

Let \(P_k\) be the path on \(k\) vertices and \(\ell=\lfloor\frac{k-1}{2}\rfloor\). If \(n\geq k\geq 5\) then is \(\mathrm{AR}(n,P_k)\) equal to \(\max\left(\binom{k-2}{2}+1, \binom{\ell-1}{2}+(\ell-1)(n-\ell+1)+\epsilon\right)\)where \(\epsilon=1\) if \(k\) is odd and \(\epsilon=2\) otherwise?

A proof of the formula for \(\mathrm{AR}(n,P_k)\) for all \(n\geq k\geq 5\) has been announced by Yuan [Yu21].

theorem erdos_1105.parts.ii :
    ∀ (k n : ℕ), 5 ≤ k → k ≤ n →
    let ℓ := (k - 1) / 2
    let ε := if Odd k then 1 else 2
    antiRamseyNum (pathGraph k) n = max ((k - 2).choose 2 + 1) ((ℓ - 1).choose 2 +
      (ℓ - 1) * (n - ℓ + 1) + ε)

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

Sources

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

LeanErdos1105.erdos_1105.parts.i · Erdos1105.erdos_1105.parts.ii

TheoremErdős Problem 1106#

References: - erdosproblems.com/1106 - [ScWi87] Schinzel, A. and Wirsing, E., Multiplicative properties of the partition function. Proc. Indian Acad. Sci. Math. Sci. (1987), 297--303.

Quoted from FormalConjectures/ErdosProblems/1106.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/1106.

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

Erdos1106.erdos_1106.parts.i

Solved: stated here without proof.

Let \(p(n)\) be the partition number of \(n\) and \(F(n)\) be the number of distinct prime factors of \(\prod_{i= 1} ^ {n} p(n)\), then \(F(n)\) tends to infinity when \(n\) tends to infinity.

The answer is yes: Schinzel and Wirsing [ScWi87] proved \(F(n) \gg \log n\).

theorem erdos_1106.parts.i :
    Tendsto (fun n ↦ #(∏ i ∈ Icc 1 n, partitionNumber i).primeFactors) atTop atTop

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

Erdos1106.erdos_1106.parts.ii

Open: stated without proof.

Let \(p(n)\) be the partition number of \(n\) and \(F(n)\) be the number of distinct prime factors of \(\prod_{i= 1} ^ {n} p(n)\), \(F(n)>n\) for sufficiently large \(n\).

theorem erdos_1106.parts.ii :
    ∀ᶠ n in atTop, #(∏ i ∈ Icc 1 n, partitionNumber i).primeFactors > n

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

Sources

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

LeanErdos1106.erdos_1106.parts.i · Erdos1106.erdos_1106.parts.ii

TheoremErdős Problem 1107#

References: - erdosproblems.com/1107 - [He88] Heath-Brown, D. R., Ternary quadratic forms and sums of three square-full numbers. (1988)

Quoted from FormalConjectures/ErdosProblems/1107.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/1107.

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

Erdos1107.erdos_1107

Open: stated without proof.

Let \(r \ge 2\). Is every large integer the sum of at most \(r + 1\) many \(r\)-powerful numbers?

theorem erdos_1107 : ∀ r ≥ 2, ∀ᶠ n in atTop, SumOfRPowerful r n

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

Erdos1107.erdos_1107.variants.two

Solved: stated here without proof.

Heath-Brown [He88] proved every large integer the sum of at most three \(2\)-powerful numbers.

theorem erdos_1107.variants.two : ∀ᶠ n in atTop, SumOfRPowerful 2 n

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

Sources

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

LeanErdos1107.erdos_1107 · Erdos1107.erdos_1107.variants.two

TheoremErdős Problem 1108#

Reference: erdosproblems.com/1108

Quoted from FormalConjectures/ErdosProblems/1108.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/1108.

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

Erdos1108.erdos_1108.parts.i

Open: stated without proof.

For each \(k \geq 2\), does the set \(A = \left\{ \sum_{n\in S}n! : S\subset \mathbb{N}_{\geq 1}\text{ finite}\right\}\) of all finite sums of distinct factorials contain only finitely many \(k\)-th powers?

theorem erdos_1108.parts.i : ∀ k ≥ 2,
    Set.Finite { a | a ∈ FactorialSums ∧ ∃ m : ℕ, m ^ k = a }

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

Erdos1108.erdos_1108.parts.ii

Open: stated without proof.

Does the set \(A = \left\{ \sum_{n\in S}n! : S\subset \mathbb{N}_{\geq 1}\text{ finite}\right\}\) of all finite sums of distinct factorials contain only finitely many powerful numbers (Nat.Powerful)?

theorem erdos_1108.parts.ii :
     {a ∈ FactorialSums | a.Powerful}.Finite

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

Sources

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

LeanErdos1108.erdos_1108.parts.i · Erdos1108.erdos_1108.parts.ii

TheoremErdős Problem 1109#

References: - erdosproblems.com/1109 - [ErSa87] P. Erdős and A. Sárközy, On divisibility properties of integers of the form \(a+a'\), Acta Math. Hungar. (1987), 117--122. - [Gy01] Katalin Gyarmati, On divisibility properties of integers of the form \(ab+1\), Period. Math. Hungar. (2001), 71--79. - [Ko04] S. V. Konyagin, Problems of the set of square-free numbers, Izv. Ross. Akad. Nauk Ser. Mat. (2004), 63--90. - [Sa92c] G. N. Sárközy, On a problem of P. Erdős, Acta Math. Hungar. (1992), 271--282.

Quoted from FormalConjectures/ErdosProblems/1109.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/1109.

The file states 6 research or textbook statements: 2 open and 4 solved.

Erdos1109.erdos_1109

Open: stated without proof.

Let \(f(N)\) be the size of the largest subset \(A\subseteq \{1,\ldots,N\}\) such that every \(n\in A+A\) is squarefree. Estimate \(f(N)\). In particular, is it true that \(f(N)\leq N^{o(1)}\), or even \(f(N) \leq (\log N)^{O(1)}\)?

This theorem formalizes the subpolynomial bound as f(N) = O(N^ε) for every ε > 0.

theorem erdos_1109 :
    ∀ ε > (0 : ℝ),
      (fun N : ℕ => (f N : ℝ)) ≪ fun N : ℕ => (N : ℝ) ^ ε

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1109.lean, line 58.

Erdos1109.erdos_1109.variants.polylog

Open: stated without proof.

Is the stronger polylogarithmic bound \(f(N) \leq (\log N)^{O(1)}\) true?

theorem erdos_1109.variants.polylog :
    ∃ C > (0 : ℝ),
      (fun N : ℕ => (f N : ℝ)) ≪ fun N : ℕ => (Real.log N) ^ C

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1109.lean, line 67.

Erdos1109.erdos_1109.variants.erdos_sarkozy_lower

Solved: stated here without proof.

Erdős and Sárközy [ErSa87] proved the lower bound \(\log N \ll f(N)\).

theorem erdos_1109.variants.erdos_sarkozy_lower :
    (fun N : ℕ => Real.log N) ≪ fun N : ℕ => (f N : ℝ)

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

Erdos1109.erdos_1109.variants.erdos_sarkozy_upper

Solved: stated here without proof.

Erdős and Sárközy [ErSa87] proved the upper bound \(f(N) \ll N^{3/4}\log N\).

theorem erdos_1109.variants.erdos_sarkozy_upper :
    (fun N : ℕ => (f N : ℝ)) ≪
      fun N : ℕ => (N : ℝ) ^ ((3 : ℝ) / 4) * Real.log N

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

Erdos1109.erdos_1109.variants.konyagin_lower

Solved: stated here without proof.

Konyagin [Ko04] improved the lower bound to \(\log\log N(\log N)^2 \ll f(N)\).

theorem erdos_1109.variants.konyagin_lower :
    (fun N : ℕ => Real.log (Real.log N) * (Real.log N) ^ 2) ≪
      fun N : ℕ => (f N : ℝ)

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

Erdos1109.erdos_1109.variants.konyagin_upper

Solved: stated here without proof.

Konyagin [Ko04] improved the upper bound to \(f(N) \ll N^{11/15+o(1)}\).

theorem erdos_1109.variants.konyagin_upper :
    ∀ ε > (0 : ℝ), (fun N : ℕ => (f N : ℝ)) ≪
      fun N : ℕ => (N : ℝ) ^ ((11 : ℝ) / 15 + ε)

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

Sources

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

LeanErdos1109.erdos_1109 · Erdos1109.erdos_1109.variants.polylog · Erdos1109.erdos_1109.variants.erdos_sarkozy_lower · Erdos1109.erdos_1109.variants.erdos_sarkozy_upper · Erdos1109.erdos_1109.variants.konyagin_lower · Erdos1109.erdos_1109.variants.konyagin_upper

TheoremErdős Problem 1110#

Reference: Erdős Problem 1110

Quoted from FormalConjectures/ErdosProblems/1110.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/1110.

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

Erdos1110.erdos_1110

Open: stated without proof.

Let \(p>q\geq 2\) be two coprime integers. We call \(n\) representable if it is the sum of integers of the form \(p^kq^l\), none of which divide each other.

If \(\{p,q\}\neq \{2,3\}\) then what can be said about the density of non-representable numbers? Are there infinitely many coprime non-representable numbers, that is, an infinite family of pairwise coprime non-representable integers?

theorem erdos_1110 :
    ∀ (p q : ℕ), q < p → 2 ≤ q →
      Nat.Coprime p q → ¬(p = 3 ∧ q = 2) →
      ∃ A : Set ℕ, A.Infinite ∧ A.Pairwise Nat.Coprime ∧
        ∀ n ∈ A, ¬Representable p q n

Category research open; AMS 05 Combinatorics, 11 Number theory. Declared in FormalConjectures/ErdosProblems/1110.lean, line 50.

Sources

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

LeanErdos1110.erdos_1110

TheoremErdős Problem 1111#

References: - erdosproblems.com/1111 - [ElEr85] El-Zahar, M. and Erdős, P., On the existence of two non-neighboring subgraphs in a graph. Combinatorica 5 (1985), 295-300. - [NSS24] Nguyen, T., Scott, A. and Seymour, P., On a problem of El-Zahar and Erdős. J. Combin. Theory Ser. B 165 (2024), 211-222. arXiv:2303.13449 - [Wa80b] Wagon, S., A bound on the chromatic number of graphs without certain induced subgraphs. J. Combin. Theory Ser. B 29 (1980), 345-346.

Quoted from FormalConjectures/ErdosProblems/1111.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/1111.

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

Erdos1111.erdos_1111

Open: stated without proof.

If \(G\) is a finite graph and \(A,B\) are disjoint sets of vertices then we call \(A,B\) anticomplete if there are no edges between \(A\) and \(B\).

If \(t,c\geq 1\) then there exists \(d\geq 1\) such that if \(\chi(G)\geq d\) and \(\omega(G)\lt t\) then there are anticomplete sets \(A,B\) with \(\chi(A)\geq \chi(B)\geq c\).

El-Zahar and Erdős [ElEr85] pose this as a question. Here \(\chi(A)\) is the chromatic number of the induced subgraph \(G[A]\). Swapping \(A\) and \(B\), the conclusion says that both \(\chi(A)\) and \(\chi(B)\) are at least \(c\).

theorem erdos_1111 :
    ∀ t c : ℕ, 1 ≤ t → 1 ≤ c → ∃ d : ℕ, 1 ≤ d ∧
      ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
        (d : ℕ∞) ≤ G.chromaticNumber → G.CliqueFree t →
          ∃ A B : Set V, Anticomplete G A B ∧
            (c : ℕ∞) ≤ (G.induce A).chromaticNumber ∧
            (c : ℕ∞) ≤ (G.induce B).chromaticNumber

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

Erdos1111.erdos_1111.variants.wagon

Solved: stated here without proof.

El-Zahar and Erdős note that a result of Wagon [Wa80b] implies \(d(t,2)\leq \binom{t}{2}+1\), where \(d(t,c)\) is the minimal \(d\) in the problem.

theorem erdos_1111.variants.wagon (t : ℕ) :
    ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
      ((t.choose 2 + 1 : ℕ) : ℕ∞) ≤ G.chromaticNumber → G.CliqueFree t →
        ∃ A B : Set V, Anticomplete G A B ∧
          2 ≤ (G.induce A).chromaticNumber ∧ 2 ≤ (G.induce B).chromaticNumber

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

Erdos1111.erdos_1111.variants.el_zahar_erdos

Solved: stated here without proof.

El-Zahar and Erdős [ElEr85] proved the case \(c = 3\): \(d(t,3)\) exists for every \(t\).

theorem erdos_1111.variants.el_zahar_erdos :
    ∀ t : ℕ, 1 ≤ t → ∃ d : ℕ, 1 ≤ d ∧
      ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
        (d : ℕ∞) ≤ G.chromaticNumber → G.CliqueFree t →
          ∃ A B : Set V, Anticomplete G A B ∧
            3 ≤ (G.induce A).chromaticNumber ∧ 3 ≤ (G.induce B).chromaticNumber

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

Erdos1111.erdos_1111.variants.three_three

Solved: stated here without proof.

El-Zahar and Erdős [ElEr85] proved \(d(3,3)\leq 8\).

theorem erdos_1111.variants.three_three :
    ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
      8 ≤ G.chromaticNumber → G.CliqueFree 3 →
        ∃ A B : Set V, Anticomplete G A B ∧
          3 ≤ (G.induce A).chromaticNumber ∧ 3 ≤ (G.induce B).chromaticNumber

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

Erdos1111.erdos_1111.variants.nguyen_scott_seymour

Solved: stated here without proof.

Nguyen, Scott, and Seymour [NSS24] prove that if \(t,c\geq 1\) then there exists \(d\geq 1\) such that if \(\chi(G)\geq d\) and \(\omega(G)\lt t\) then there are anticomplete sets \(A,B\) with \(\chi(B)\geq c\) and such that the minimum degree of the induced graph on \(A\) is at least \(c\).

theorem erdos_1111.variants.nguyen_scott_seymour :
    ∀ t c : ℕ, 1 ≤ t → 1 ≤ c → ∃ d : ℕ, 1 ≤ d ∧
      ∀ (V : Type*) [Finite V] (G : SimpleGraph V),
        (d : ℕ∞) ≤ G.chromaticNumber → G.CliqueFree t →
          ∃ A B : Set V, Anticomplete G A B ∧
            A.Nonempty ∧ (∀ v ∈ A, c ≤ (A ∩ G.neighborSet v).ncard) ∧
            (c : ℕ∞) ≤ (G.induce B).chromaticNumber

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

Sources

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

LeanErdos1111.erdos_1111 · Erdos1111.erdos_1111.variants.wagon · Erdos1111.erdos_1111.variants.el_zahar_erdos · Erdos1111.erdos_1111.variants.three_three · Erdos1111.erdos_1111.variants.nguyen_scott_seymour

TheoremErdős Problem 1113#

References: - erdosproblems.com/1113 - [ErGr80] Erdős, P. and Graham, R. L., Old and New Problems and Results in Combinatorial Number Theory. Monographie de l'Enseignement Mathématique, No. 28 (1980). - [Si60] Sierpiński, W., Elementary Theory of Numbers. Państwowe Wydawnictwo Naukowe, Warsaw (1960). - [FFK08] Filaseta, M., Finch, C., and Kozek, M., On powers associated with Sierpiński numbers, Riesel numbers and Polignac's conjecture. Journal of Number Theory 128 (2008), 1916–1940.

A positive odd integer \(k\) is a Sierpiński number if \(k \cdot 2^n + 1\) is composite for all \(n \geq 0\). A covering set for \(k\) is a finite set of primes \(P\) such that every number of the form \(k \cdot 2^n + 1\) is divisible by at least one prime in \(P\).

Sierpiński (1960) proved that infinitely many Sierpiński numbers exist using covering systems. The smallest known Sierpiński number is 78557 (Selfridge). Erdős and Graham conjectured that there exist Sierpiński numbers with no finite covering set. A negative answer would imply infinitely many Fermat primes.

Note: The notion of a covering set for a Sierpiński number is closely related to a CoveringSystem of \(\mathbb{Z}\) (see FormalConjecturesForMathlib.NumberTheory.CoveringSystem): a finite covering set of primes for \(k\) works because the exponents \(n\) for which each prime divides \(k \cdot 2^n + 1\) form residue classes whose union covers all of \(\mathbb{Z}\), i.e. a covering system.

See also Erdős Problems 203 and 276.

Quoted from FormalConjectures/ErdosProblems/1113.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/1113.

The file states 3 research or textbook statements: 2 open and 1 solved.

Erdos1113.erdos_1113.variants.infinitely_many_sierpinski

Solved: stated here; a Lean proof is at https://github.com/HowieHwong/lean-erdos-proofs/blob/b8b641ba2d00dc4d1fe205a078a4159372672459/Erdos/P1113.lean#L22.

Sierpiński [Si60] proved that there are infinitely many Sierpiński numbers, using covering systems to construct suitable covering sets for any \(k\) satisfying a certain congruence.

theorem erdos_1113.variants.infinitely_many_sierpinski :
    Set.Infinite {k : ℕ | k.IsSierpinskiNumber}

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

Erdos1113.erdos_1113

Open: stated without proof.

Erdős Problem 1113. Do there exist Sierpiński numbers that possess no finite covering set of primes?

Erdős and Graham [ErGr80] conjectured that the answer is yes. A negative answer would imply that there are infinitely many Fermat primes.

theorem erdos_1113 :
    ∃ k, k.IsSierpinskiNumber ∧ ¬ HasFinitePrimeCoveringSet k

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

Erdos1113.erdos_1113.variants.filaseta_finch_kozek

Open: stated without proof.

Filaseta–Finch–Kozek conjecture (2008). Every Sierpiński number is either a perfect power or possesses a finite covering set of primes.

theorem erdos_1113.variants.filaseta_finch_kozek :
    ∀ k, k.IsSierpinskiNumber →
      k.IsPerfectPower ∨ HasFinitePrimeCoveringSet k

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

Sources

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

LeanErdos1113.erdos_1113.variants.infinitely_many_sierpinski · Erdos1113.erdos_1113 · Erdos1113.erdos_1113.variants.filaseta_finch_kozek

TheoremErdős Problem 1114#

References: - erdosproblems.com/1114 - [Ba60b] Bálint, Elemér, Proof of a conjecture of P. Erdős (Hungarian: Erdős Pál egy sejtésének bizonyítása). Mat. Lapok 11 (1960), 33-40. - [Lo76] Lorch, L., Some monotonicity properties of polynomials with equally spaced zeros. Acta Math. Acad. Sci. Hungar. 27 (1976), 293-300.

Quoted from FormalConjectures/ErdosProblems/1114.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/1114.

The file states 2 research or textbook statements: 1 solved and 1 textbook result.

Erdos1114.erdos_1114

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

Let \(f(x)\in \mathbb{R}[x]\) be a polynomial of degree \(n\) whose roots \(\{a_0\lt \cdots\lt a_n\}\) are all real and form an arithmetic progression.

The differences between consecutive zeros of \(f'(x)\), beginning from the midpoint of \((a_0,a_n)\) towards the endpoints, are monotonically increasing.

Proved by Bálint [Ba60b]; some generalisations were given by Lorch [Lo76]. We take \(f\) of degree \(N+1\) with the \(N+1\) roots \(a+jd\) (\(0\le j\le N\), \(d>0\)), since the number of roots must equal the degree, and read "increasing" as non-decreasing. Here b k is the zero of \(f'\) in \((a+kd,a+(k+1)d)\), which exists and is the only zero there by Rolle's theorem (see erdos_1114.variants.rolle).

theorem erdos_1114 {N : ℕ} (hN : 0 < N) {a d : ℝ} (hd : 0 < d) {f : ℝ[X]} {b : ℕ → ℝ}
    (hdegree : f.natDegree = N + 1)
    (hroots : ∀ j : ℕ, j ≤ N → f.eval (a + d * j) = 0)
    (hb : ∀ k : ℕ, k < N → b k ∈ Set.Ioo (a + d * k) (a + d * (k + 1)))
    (hderiv : ∀ k : ℕ, k < N → f.derivative.eval (b k) = 0) :
    RightGapMonotone N b ∧ GapSymmetric N b

Category research solved; AMS 12 Field theory and polynomials, 26 Real functions. Declared in FormalConjectures/ErdosProblems/1114.lean, line 70.

Erdos1114.erdos_1114.variants.rolle

Textbook result, stated without proof.

All the zeros of \(f'(x)\) are all distinct real numbers in \((a_0,a_n)\) by Rolle's theorem.

Precisely, for \(f\) as in erdos_1114 (degree \(N+1\), roots \(a+jd\) for \(0\le j\le N\)), each interval \((a+kd,a+(k+1)d)\) with \(k\lt N\) contains exactly one zero of \(f'\), and every zero of \(f'\) lies in one of these intervals.

theorem erdos_1114.variants.rolle {N : ℕ} {a d : ℝ} (hd : 0 < d) {f : ℝ[X]}
    (hdegree : f.natDegree = N + 1)
    (hroots : ∀ j : ℕ, j ≤ N → f.eval (a + d * j) = 0) :
    (∀ k : ℕ, k < N →
      ∃! x : ℝ, x ∈ Set.Ioo (a + d * k) (a + d * (k + 1)) ∧ f.derivative.eval x = 0) ∧
    (∀ x : ℝ, f.derivative.eval x = 0 →
      ∃ k : ℕ, k < N ∧ x ∈ Set.Ioo (a + d * k) (a + d * (k + 1)))

Category textbook; AMS 12 Field theory and polynomials, 26 Real functions. Declared in FormalConjectures/ErdosProblems/1114.lean, line 86.

Sources

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

LeanErdos1114.erdos_1114 · Erdos1114.erdos_1114.variants.rolle

TheoremErdős Problem 1115#

References: - erdosproblems.com/1115 - [Ha74] Hayman, W. K., Research problems in function theory: new problems. Proceedings of the Symposium on Complex Analysis (Canterbury, 1973), London Math. Soc. Lecture Note Ser. 12 (1974), 155--180. - [HaLi18] Hayman, W. K. and Lingham, E. F., Research problems in function theory. arXiv:1809.07200 (2018). - [GoEr79] Gol'dberg, A. A. and Erëmenko, A. È., On asymptotic curves of entire functions of finite order. Mat. Sb. (N.S.) (1979), 555--581, 647. English translation: Math. USSR-Sb. 37 (1980), 509--533. Math-Net.Ru - [Ha60b] Hayman, W. K., Slowly growing integral and subharmonic functions. Comment. Math. Helv. 34 (1960), 75--84.

Quoted from FormalConjectures/ErdosProblems/1115.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/1115.

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

Erdos1115.erdos_1115

Solved: stated here without proof.

Let \(f(z)\) be an entire function of finite order, and let \(\Gamma\) be a rectifiable path on which \(f(z)\to \infty\). Let \(\ell(r)\) be the length of \(\Gamma\) in the disc \(\lvert z\rvert\lt r\).

Find a path for which \(\ell(r)\) grows as slowly as possible, and estimate \(\ell(r)\) in terms of \(M(r)=\max_{\lvert z\rvert=r}\lvert f(z)\rvert\).

In particular, can such a path \(\Gamma\) be found for which \(\ell(r)\ll r\)?

This is Problem 2.41 of [Ha74], where it is attributed to Erdős; see also [HaLi18, Problem 2.41]. The answer is no: Gol'dberg and Eremenko [GoEr79] proved that for every \(\rho\in[0,\infty]\) there is an entire function \(f\) of order \(\rho\) such that, for any asymptotic curve \(\Gamma\) on which \(f\to\infty\), the length of \(\Gamma\) in \(\lvert z\rvert\leq r\) is not \(O(r)\) (see also [HaLi18, Updates 2.7 and 2.41]). The length in \(\lvert z\rvert\leq r\) is at most the length in \(\lvert z\rvert<2r\), so \(\ell(r)=O(r)\) for the open disc used here would make the length in the closed disc \(O(r)\) too.

We formalise the last question only: the first part asks for a best possible path and an estimate in terms of \(M(r)\) and has no precise claim to state, so it is not formalised. Reading choices: \(f\) is non-constant (a constant has no path on which \(f\to\infty\), which would make the statement trivially true); finite order is Erdos516.OfFiniteOrder; \(\Gamma\) is given by its arc length parametrisation γ (every rectifiable path on which \(f\to\infty\) has infinite length and can be reparametrised by arc length, without changing the curve traversed or the length in any disc); \(\ell(r)\ll r\) means \(\ell(r)\le Cr\) for some \(C\) and all large \(r\).

[HaLi18, Problem 2.41] also report that Hayman [Ha60b] (and Piranian) showed that if \(\log M(r)=O((\log r)^2)\), one can take for \(\Gamma\) a ray from the origin, so that \(\ell(r)=r\).

theorem erdos_1115 :
    ¬ ∀ f : ℂ → ℂ, Erdos516.OfFiniteOrder f → (¬ ∃ a : ℂ, ∀ z, f z = a) →
      ∃ γ : ℝ → ℂ, IsAsymptoticPath f γ ∧
        ∃ C : ℝ, ∀ᶠ r : ℝ in atTop, lengthInDisc γ r ≤ ENNReal.ofReal (C * r)

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1115.lean, line 99.

Sources

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

LeanErdos1115.erdos_1115

TheoremErdős Problem 1116#

References: - erdosproblems.com/1116 - [Ha74] Hayman, W. K., Research problems in function theory: new problems. Proceedings of the Symposium on Complex Analysis (Canterbury, 1973), London Math. Soc. Lecture Note Ser. 12 (1974), 155--180. - [To76] Toppila, Sakari, On the counting function for the \(a\)-values of a meromorphic function. Ann. Acad. Sci. Fenn. Ser. A I Math. 2 (1976), 565--572. PDF - [Go78] Gol'dberg, A. A., Counting functions of sequences of \(a\)-points for entire functions. Sibirsk. Mat. Zh. 19 (1978), 28--36, 236. - [HaLi18] Hayman, W. K. and Lingham, E. F., Research problems in function theory. arXiv:1809.07200 (2018).

Quoted from FormalConjectures/ErdosProblems/1116.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/1116.

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

Erdos1116.erdos_1116

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

For a meromorphic function \(f\) let \(n(r,a)\) count the number of roots of \(f(z)=a\) in the disc \(\lvert z\rvert \lt r\). Does there exist a meromorphic (or entire) \(f\) such that for every \(a\neq b\)

\[\limsup_{r\to \infty}\frac{n(r,a)}{n(r,b)}=\infty?\]

This is Problem 1.25 in [Ha74], where it is attributed to Erdős. Gol'dberg [Go78] and Toppila [To76, Theorem 3] constructed such entire functions. We state this case, for finite \(a\neq b\), using UnboundedCountRatio.

theorem erdos_1116 :
    ∃ f : ℂ → ℂ, Differentiable ℂ f ∧
      ∀ a b : ℂ, a ≠ b → UnboundedCountRatio f a b

Category research solved; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1116.lean, line 77.

Sources

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

LeanErdos1116.erdos_1116

TheoremErdős Problem 1119#

References: - erdosproblems.com/1119 - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180. - [Er64g] Erdős, P., An interpolation problem associated with the continuum hypothesis. Michigan Math. J. (1964), 9--10. - [KuSh17] Kumar, Ashutosh and Shelah, Saharon, On a question about families of entire functions. Fund. Math. (2017), 279--288. - [ScWe24] Schilhan, Jonathan and Weinert, Thilo, Wetzel families and the continuum. J. Lond. Math. Soc. (2) (2024), Paper No. e12918, 27.

Quoted from FormalConjectures/ErdosProblems/1119.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/1119.

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

Erdos1119.erdos_1119

Solved: stated here without proof.

Let \(\mathfrak{m}\) be an infinite cardinal with \(\aleph_0 < \mathfrak{m} < \mathfrak{c} = 2^{\aleph_0}\). Let \(\{f_\alpha\}\) be a family of entire functions such that, for every \(z_0 \in \mathbb{C}\), there are at most \(\mathfrak{m}\) distinct values of \(f_\alpha(z_0)\). Must \(\{f_\alpha\}\) have cardinality at most \(\mathfrak{m}\)?

This is Problem 2.46 in [Ha74], where it is attributed to Erdős. The question is independent of ZFC: the headline statement is neither provable nor refutable from the usual axioms of set theory, so its sorry cannot be filled either way.

The answer is yes if \(\mathfrak{m}^+ < \mathfrak{c}\) (see erdos_1119.variants.easy_case), so the question reduces to the case \(\mathfrak{m}^+ = \mathfrak{c}\), where it is undecidable: Kumar and Shelah [KuSh17] produced a model of \(\mathfrak{c} = \aleph_2\) in which the answer is yes (with \(\mathfrak{m} = \aleph_1\)), while Schilhan and Weinert [ScWe24] produced a different model of \(\mathfrak{c} = \aleph_2\) in which the answer is no.

theorem erdos_1119 :
    ∀ (m : Cardinal.{0}), ℵ₀ < m → m < 𝔠 →
    ∀ F : Set (ℂ → ℂ), (∀ f ∈ F, Differentiable ℂ f) →
      (∀ z₀ : ℂ, #{y : ℂ | ∃ f ∈ F, f z₀ = y} ≤ m) →
      #F ≤ m

Category research solved; AMS 03 Mathematical logic and foundations, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1119.lean, line 59.

Erdos1119.erdos_1119.variants.easy_case

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

The 'easy' case of Erdős Problem 1119: if moreover \(\mathfrak{m}^+ < \mathfrak{c}\), then any family of entire functions taking at most \(\mathfrak{m}\) distinct values at each point has cardinality at most \(\mathfrak{m}\). In [Ha74] it is written that this is 'easy to see'.

theorem erdos_1119.variants.easy_case (m : Cardinal.{0}) (hm : ℵ₀ < m)
    (hsucc : succ m < 𝔠) (F : Set (ℂ → ℂ))
    (hF : ∀ f ∈ F, Differentiable ℂ f)
    (hval : ∀ z₀ : ℂ, #{y : ℂ | ∃ f ∈ F, f z₀ = y} ≤ m) :
    #F ≤ m

Category research solved; AMS 03 Mathematical logic and foundations, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1119.lean, line 92.

Erdos1119.erdos_1119.variants.erdos_wetzel

Solved: stated here without proof.

Erdős's theorem [Er64g], answering a question of Wetzel: if \(\mathfrak{c} > \aleph_1\), then every family of entire functions taking only countably many distinct values at each point \(z_0 \in \mathbb{C}\) is itself countable.

theorem erdos_1119.variants.erdos_wetzel (h : ℵ_ 1 < 𝔠) (F : Set (ℂ → ℂ))
    (hF : ∀ f ∈ F, Differentiable ℂ f)
    (hval : ∀ z₀ : ℂ, {y : ℂ | ∃ f ∈ F, f z₀ = y}.Countable) :
    F.Countable

Category research solved; AMS 03 Mathematical logic and foundations, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1119.lean, line 105.

Erdos1119.erdos_1119.variants.erdos_wetzel_ch

Solved: stated here without proof.

Erdős [Er64g] also showed that the previous statement fails under the continuum hypothesis: if \(\mathfrak{c} = \aleph_1\), then there is an uncountable family of entire functions taking only countably many distinct values at each point \(z_0 \in \mathbb{C}\).

theorem erdos_1119.variants.erdos_wetzel_ch (h : 𝔠 = ℵ_ 1) :
    ∃ F : Set (ℂ → ℂ), (∀ f ∈ F, Differentiable ℂ f) ∧
      (∀ z₀ : ℂ, {y : ℂ | ∃ f ∈ F, f z₀ = y}.Countable) ∧
      ¬ F.Countable

Category research solved; AMS 03 Mathematical logic and foundations, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1119.lean, line 118.

Sources

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

LeanErdos1119.erdos_1119 · Erdos1119.erdos_1119.variants.easy_case · Erdos1119.erdos_1119.variants.erdos_wetzel · Erdos1119.erdos_1119.variants.erdos_wetzel_ch

TheoremErdős Problem 1121#

References: - erdosproblems.com/1121 - [BeLi16] Bezdek, Károly and Litvak, Alexander E., Packing convex bodies by cylinders. Discrete Comput. Geom. (2016), 725-738. - [GoGo45] Goodman, A. W. and Goodman, R. E., A circle covering theorem. Amer. Math. Monthly (1945), 494-498. - [Ha47] Hadwiger, H., Nonseparable convex systems. Amer. Math. Monthly (1947), 583-585.

Quoted from FormalConjectures/ErdosProblems/1121.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/1121.

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

Erdos1121.erdos_1121

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1121.lean.

If \(C_1,\ldots,C_n\) are circles in \(\mathbb{R}^2\) with radii \(r_1,\ldots,r_n\) such that no line disjoint from all the circles divides them into two non-empty sets then the circles can be covered by a circle of radius \(r=\sum r_i\).

This is true, and was proved by Goodman and Goodman [GoGo45] (whose proof also generalises to higher dimensions). A generalisation to convex bodies was proved by Hadwiger [Ha47].

An alternative proof is given by Bezdek and Litvak [BeLi16].

theorem erdos_1121 {n : ℕ} (c : Fin n → ℝ²) (r : Fin n → ℝ) (hr : ∀ i, 0 < r i)
    (hsep : ∀ (v : ℝ²) (t : ℝ), v ≠ 0 →
      (∀ i, ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) →
      (∀ i, inner ℝ v (c i) < t) ∨ (∀ i, t < inner ℝ v (c i))) :
    ∃ z : ℝ², (⋃ i, Metric.closedBall (c i) (r i)) ⊆ Metric.closedBall z (∑ i, r i)

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1121.lean, line 50.

Erdos1121.erdos_1121.variants.higher_dimension

Solved: stated here without proof.

The proof of Goodman and Goodman [GoGo45] also generalises to higher dimensions: if \(B_1,\ldots,B_n\) are balls in \(\mathbb{R}^d\) with radii \(r_1,\ldots,r_n\) such that no hyperplane disjoint from all the balls divides them into two non-empty sets then the balls can be covered by a ball of radius \(r=\sum r_i\).

theorem erdos_1121.variants.higher_dimension {d n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin d))
    (r : Fin n → ℝ) (hr : ∀ i, 0 < r i)
    (hsep : ∀ (v : EuclideanSpace ℝ (Fin d)) (t : ℝ), v ≠ 0 →
      (∀ i, ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) →
      (∀ i, inner ℝ v (c i) < t) ∨ (∀ i, t < inner ℝ v (c i))) :
    ∃ z : EuclideanSpace ℝ (Fin d),
      (⋃ i, Metric.closedBall (c i) (r i)) ⊆ Metric.closedBall z (∑ i, r i)

Category research solved; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/1121.lean, line 64.

Sources

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

LeanErdos1121.erdos_1121 · Erdos1121.erdos_1121.variants.higher_dimension

TheoremErdős Problem 1122#

References: - erdosproblems.com/1122 - [Er46] Erdős, P., On the distribution function of additive functions. Annals of Math. (1946), 1-20. - [Ma22] Mangerel, Alexander P., Additive functions in short intervals, gaps and a conjecture of Erdős. Ramanujan J. (2022), 1023--1090.

Quoted from FormalConjectures/ErdosProblems/1122.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/1122.

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

Erdos1122.erdos_1122

Open: stated without proof.

Let \(f:\mathbb{N}\to \mathbb{R}\) be an additive function (i.e. \(f(ab)=f(a)+f(b)\) whenever \((a,b)=1\)). Let

\[A=\{ n \geq 1: f(n+1)< f(n)\}.\]

If \(\lvert A\cap [1,X]\rvert =o(X)\) then must \(f(n)=c\log n\) for some \(c\in \mathbb{R}\)?

The condition \(\lvert A\cap [1,X]\rvert =o(X)\) says that \(A\) has natural density \(0\).

Partial progress was made by Mangerel [Ma22], who proved that this is true for completely additive \(f\) if

\[\lvert A\cap [1,X]\rvert \ll \frac{X}{(\log X)^{2+c}}\]

for some \(c>0\), and if \(f(p)\) does not have very large values (in a certain technical sense).

See also erdos_491.

theorem erdos_1122 : ∀ f : ℕ → ℝ,
    (∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b) →
    {n | 1 ≤ n ∧ f (n + 1) < f n}.HasDensity 0 →
    ∃ c : ℝ, ∀ n > 0, f n = c * Real.log n

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

Erdos1122.erdos_1122.variants.monotone

Solved: stated here without proof.

Erdős [Er46] proved that \(f(n)=c\log n\) for some \(c\in\mathbb{R}\) if \(A\) is empty, that is, if \(f(n) \leq f(n+1)\) for all \(n \geq 1\).

theorem erdos_1122.variants.monotone (f : ℕ → ℝ)
    (hf : ∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b)
    (hmono : ∀ n ≥ 1, f n ≤ f (n + 1)) :
    ∃ c : ℝ, ∀ n > 0, f n = c * Real.log n

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

Erdos1122.erdos_1122.variants.sub_tendsto_zero

Solved: stated here without proof.

Erdős [Er46] proved that \(f(n)=c\log n\) for some \(c\in\mathbb{R}\) if \(f(n+1)-f(n)=o(1)\).

theorem erdos_1122.variants.sub_tendsto_zero (f : ℕ → ℝ)
    (hf : ∀ᵉ (a > 0) (b > 0), a.Coprime b → f (a * b) = f a + f b)
    (hdiff : Tendsto (fun n ↦ f (n + 1) - f n) atTop (𝓝 0)) :
    ∃ c : ℝ, ∀ n > 0, f n = c * Real.log n

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

Sources

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

LeanErdos1122.erdos_1122 · Erdos1122.erdos_1122.variants.monotone · Erdos1122.erdos_1122.variants.sub_tendsto_zero

TheoremErdős Problem 1125#

References: - erdosproblems.com/1125 - [Er81b] Erdős, P., My Scottish Book 'Problems'. The Scottish Book (1981), 27-35. - [Ke69] Kemperman, J. H. B., On the regularity of generalized convex functions. Trans. Amer. Math. Soc. (1969), 69-93. - [La84] Laczkovich, M., On Kemperman's inequality \(2f(x)\leq f(x+h)+f(x+2h)\). Colloq. Math. (1984), 109-115.

Quoted from FormalConjectures/ErdosProblems/1125.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/1125.

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

Erdos1125.erdos_1125

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1125.lean.

Let \(f:\mathbb{R}\to \mathbb{R}\) be such that

\[2f(x) \leq f(x+h)+f(x+2h)\]

for every \(x\in \mathbb{R}\) and \(h>0\). Must \(f\) be monotonic?

A problem of Kemperman [Ke69], who proved it is true if \(f\) is measurable. Erdős [Er81b] wrote 'if it were my problem I would offer $500 for it'. This was solved by Laczkovich [La84].

theorem erdos_1125 : ∀ (f : ℝ → ℝ)
    (hf : ∀ x : ℝ, ∀ h : ℝ, h > 0 → 2 * f x ≤ f (x + h) + f (x + 2 * h)),
    Monotone f

Category research solved; AMS 26 Real functions. Declared in FormalConjectures/ErdosProblems/1125.lean, line 43.

Sources

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

LeanErdos1125.erdos_1125

TheoremErdős Problem 1126#

References: - erdosproblems.com/1126 - [Er60c] Erdős, P., Problem 310. Colloq. Math., 311. - [dB66] de Bruijn, N. G., On almost additive functions. Colloq. Math. (1966), 59-63. - [Ju65] Jurkat, Wolfgang B., On Cauchy's functional equation. Proc. Amer. Math. Soc. (1965), 683-686.

Quoted from FormalConjectures/ErdosProblems/1126.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/1126.

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

Erdos1126.erdos_1126

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1126.lean.

If

\[f(x+y)=f(x)+f(y)\]

for almost all \(x,y\in \mathbb{R}\) then there exists a function \(g\) such that

\[g(x+y)=g(x)+g(y)\]

for all \(x,y\in\mathbb{R}\) such that \(f(x)=g(x)\) for almost all \(x\).

Proved independently by de Bruijn [dB66] and Jurkat [Ju65].

theorem erdos_1126 : ∀
    (f : ℝ → ℝ)
    (h :
      ∀ᵐ (p : ℝ × ℝ) ∂(volume.prod volume),
        f (p.1 + p.2) = f p.1 + f p.2),
    ∃ h : ℝ → ℝ,
      (∀ x y, h (x + y) = h x + h y) ∧ (∀ᵐ x ∂volume, f x = h x)

Category research solved; AMS 26 Real functions, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1126.lean, line 47.

Sources

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

LeanErdos1126.erdos_1126

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.