Erdős Problem 224 to Erdős Problem 244

TheoremErdős Problem 224#

References: - erdosproblems.com/224 - [DaGr62] Danzer, L. and Gr\"{u}nbaum, B., \"{U}ber zwei Probleme bez\"{u}glich konvexer K\"{o}rper von P. Erd\H{o}s und von V. L. Klee. Math. Z. (1962), 95-99.

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

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

Erdos224.erdos_224

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

If \(A\subseteq \mathbb{R}^d\) is any set of \(2^d+1\) points then some three points in \(A\) determine an obtuse angle.

The general case was proved by Danzer and Gr\"{u}nbaum [DaGr62].

theorem erdos_224 {d : ℕ} (A : Finset (ℝ^d)) (hcard : A.card = 2 ^ d + 1) :
    ∃ x y z : ℝ^d, x ∈ A ∧ y ∈ A ∧ z ∈ A ∧
      x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ ObtuseAt x y z

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

Sources
LeanErdos224.erdos_224

TheoremErdős Problem 225#

References: - erdosproblems.com/225 - [Er40b] Erdős, P., Note on some elementary properties of polynomials. Bull. Amer. Math. Soc. (1940), 954-958. - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155-180. - [Kr74] Kristiansen, G. K., Proof of an inequality for trigonometric polynomials. Proc. Amer. Math. Soc. (1974), 49-57. - [SaSh74] Saff, E. B. and Sheil-Small, T., Coefficient and integral mean estimates for algebraic and trigonometric polynomials with restricted zeros. J. London Math. Soc. (2) (1974/75), 16-22. - [Kr76] Kristiansen, G. K., Erratum to "Proof of a polynomial conjecture". Proc. Amer. Math. Soc. (1976), 377.

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

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

Erdos225.erdos_225

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

Let

\[ f(\theta) = \sum_{0\leq k\leq n}c_k e^{ik\theta}\]

be a trigonometric polynomial all of whose roots are real, such that \(\max_{\theta\in [0,2\pi]}\lvert f(\theta)\rvert=1\). Then

\[\int_0^{2\pi}\lvert f(\theta)\rvert \mathrm{d}\theta \leq 4.\]

This is Problem 4.20 in [Ha74], where it is attributed to Erdős.

This was solved independently by Kristiansen [Kr74] (only in the case when \(c_k\in\mathbb{R}\)) and Saff and Sheil-Small [SaSh74] (for general \(c_k\in \mathbb{C}\)). (The original proof of Kristiansen contained an error which was later fixed in [Kr76].)

"All roots real" refers to the zeros of \(f\) as an entire function of \(\theta\in\mathbb{C}\). We normalise by \(c_0c_n\neq 0\) and \(n\geq 1\): a factor \(e^{im\theta}\) affects neither the zeros nor \(\lvert f\rvert\) on the real line, while a single term \(c_me^{im\theta}\) has no zeros and \(\int_0^{2\pi}\lvert f\rvert = 2\pi\).

theorem erdos_225 :
    ∀ (n : ℕ) (c : ℕ → ℂ), 0 < n → c 0 ≠ 0 → c n ≠ 0 →
    (∀ z : ℂ, trigPoly n c z = 0 → z.im = 0) →
    (∀ θ ∈ Icc (0 : ℝ) (2 * Real.pi), ‖trigPoly n c θ‖ ≤ 1) →
    (∃ θ ∈ Icc (0 : ℝ) (2 * Real.pi), ‖trigPoly n c θ‖ = 1) →
    ∫ θ in (0 : ℝ)..(2 * Real.pi), ‖trigPoly n c θ‖ ≤ 4

Category research solved; AMS 30 Functions of a complex variable, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/225.lean, line 72.

Sources
LeanErdos225.erdos_225

TheoremErdős Problem 226#

References: - erdosproblems.com/226 - [BaSc70] Barth, K. F. and Schneider, W. J., Entire functions mapping countable dense subsets of the reals onto each other monotonically. J. London Math. Soc. (2) (1970), 620--626. - [BaSc71] Barth, K. F. and Schneider, W. J., Entire functions mapping arbitrary countable dense sets and their complements onto each other. J. London Math. Soc. (2) (1971/72), 482--488. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180.

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

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

Erdos226.erdos_226

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

Is there an entire non-linear function \(f\) such that, for all \(x\in\mathbb{R}\), \(x\) is rational if and only if \(f(x)\) is?

Barth and Schneider [BaSc70] proved the stronger result for countable dense subsets of \(\mathbb{R}\).

theorem erdos_226 :
    ∃ F : ℂ → ℂ, Differentiable ℂ F ∧ (∀ x : ℝ, (F x).im = 0) ∧
      (∀ g : AffineMap ℝ ℝ ℝ, (fun x : ℝ => (F x).re) ≠ g) ∧
      PreservesRationality (fun x : ℝ => (F x).re)

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

Sources
LeanErdos226.erdos_226

TheoremErdős Problem 228#

Reference: erdosproblems.com/228

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

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

Erdos228.erdos_228

Solved: stated here without proof.

Does there exist, for all large \(n\), a polynomial \(P\) of degree \(n\), with coefficients \(\pm1\), such that

\[\sqrt n \ll |P(z)| \ll \sqrt n\]

for all \(|z|=1\), with the implied constants independent of \(z\) and \(n\)?

The answer is yes, proved by Balister, Bollobás, Morris, Sahasrabudhe, and Tiba [BBMST19].

[BBMST19] Balister, P. and Bollob\'{A}s, B. and Morris, R. and Sahasrabudhe, J. and Tiba, M., Flat Littlewood Polynomials Exist. arXiv:1907.09464 (2019).

theorem erdos_228 :
    ∃ (c₁ : ℝ) (c₂ : ℝ), ∀ᶠ n : ℕ in Filter.atTop,
    ∃ p : Polynomial ℂ, p.degree = n ∧
    (∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧
    ∀ z : ℂ, ‖z‖ = 1 →
    ( √n < c₁ * ‖p.eval z‖ ∧ ‖p.eval z‖ < c₂ * √n )

Category research solved; AMS 05 Combinatorics, 12 Field theory and polynomials, 41 Approximations and expansions. Declared in FormalConjectures/ErdosProblems/228.lean, line 40.

Sources
LeanErdos228.erdos_228

TheoremErdős Problem 229#

References: - erdosproblems.com/229 - [BaSc72] Barth, K. F. and Schneider, W. J., On a problem of Erd\H{o}s concerning the zeros of the derivatives of an entire function. Proc. Amer. Math. Soc. (1972), 229--232. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180.

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

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

Erdos229.erdos_229

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

Let \((S_n)_{n \ge 1}\) be a sequence of sets of complex numbers, none of which have a finite limit point. Does there exist an entire transcendental function \(f(z)\) such that, for all \(n \ge 1\), there exists some \(k_n \ge 0\) such that \(f^{(k_n)}(z) = 0\) for all \(z \in S_n\).

This is Problem 2.30 in [Ha74], where it is attributed to Erdős.

Solved in the affirmative by Barth and Schneider [BaSc72].

This was formalized in Lean by Alexeev using Aristotle.

theorem erdos_229 :
    letI := Polynomial.algebraPi ℂ ℂ ℂ
    ∀ (S : ℕ → Set ℂ), (∀ n, derivedSet (S n) = ∅) →
    ∃ (f : ℂ → ℂ), Transcendental (Polynomial ℂ) f ∧ Differentiable ℂ f ∧ ∀ n ≥ 1,
      ∃ k, ∀ z ∈ S n, iteratedDeriv k f z = 0

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

Erdos229.theorem_1

Solved: stated here without proof.

Let \(\{S_k\}\) be any sequence of sets in the complex plane, each of which has no finite limit point. Then there exists a sequence \(\{n_k\}\) of positive integers and a transcendental entire function \(f(z)\) such that \(f^{(n_k)}(z) = 0\) if \(z \in S_k\).

theorem theorem_1
    {S : ℕ → Set ℂ}
    (h : ∀ (k), derivedSet (S k) = ∅) :
  letI := Polynomial.algebraPi ℂ ℂ ℂ
  ∃ (f : ℂ → ℂ) (n : ℕ → ℕ),
    Differentiable ℂ f ∧ Transcendental (Polynomial ℂ) f ∧ ∀ k, 0 < n k ∧ ∀ {z} (_: z ∈ S k),
      iteratedDeriv (n k) f z = 0

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

Sources
LeanErdos229.erdos_229 · Erdos229.theorem_1

TheoremErdős Problem 230#

References: - erdosproblems.com/230 - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180. - [Er80h] Erdős, P., Problems and results on polynomials and interpolation. (1980), 383--391. - [Ko80] Körner, T. W., On a polynomial of Byrnes. Bull. London Math. Soc. (1980), 219--224. - [Ka80] Kahane, Jean-Pierre, Sur les polynômes à coefficients unimodulaires. Bull. London Math. Soc. (1980), 321-342. - [BoBo09] Bombieri, Enrico and Bourgain, Jean, On Kahane's ultraflat polynomials. J. Eur. Math. Soc. (JEMS) (2009), 627-703.

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

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

Erdos230.erdos_230

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

Let \(P(z)=\sum_{1\leq k\leq n}a_kz^k\) for some \(a_k\in \mathbb{C}\) with \(\lvert a_k\rvert=1\) for \(1\leq k\leq n\). Does there exist a constant \(c>0\) such that, for \(n\geq 2\), we have

\[\max_{\lvert z\rvert=1}\lvert P(z)\rvert \geq (1+c)\sqrt{n}?\]

This is Problem 4.31 in [Ha74], in which it is described as a conjecture of Erdős and Newman. The lower bound of \(\sqrt{n}\) is trivial from Parseval's theorem. Körner [Ko80] constructed, for all \(n\geq 2\), polynomials \(P(z)=\sum_{k\leq n} a_kz^k\) with \(\lvert a_k\rvert=1\) for \(1\leq k\leq n\) such that, for all \(z\) with \(\lvert z\rvert=1\),

\[(c_1-o(1))\sqrt{n} \leq \lvert P(z)\rvert \leq (c_2+o(1))\sqrt{n}\]

for some absolute constants \(0\lt c_1\leq c_2\).

The answer is no (contrary to Erdős' initial guess). Kahane [Ka80] constructed 'ultraflat' polynomials \(P(z)=\sum a_kz^k\) with \(\lvert a_k\rvert=1\) such that

\[P(z)=(1+o(1))\sqrt{n}\]

uniformly for all \(z\in\mathbb{C}\) with \(\lvert z\rvert=1\), where the \(o(1)\) term \(\to 0\) as \(n\to \infty\).

For more details see the paper [BoBo09] of Bombieri and Bourgain and where Kahane's construction is improved to yield such a polynomial with

\[P(z)=\sqrt{n}+O(n^{\frac{7}{18}}(\log n)^{O(1)})\]

for all \(z\in\mathbb{C}\) with \(\lvert z\rvert=1\).

See also 228 and 1150.

theorem erdos_230 : ¬ ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n →
    ∀ a : Fin n → ℂ, (∀ k, ‖a k‖ = 1) → (1 + c) * √n ≤ circleMax a

Category research solved; AMS 30 Functions of a complex variable, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/230.lean, line 77.

Erdos230.erdos_230.variants.ultraflat

Solved: stated here without proof.

Kahane [Ka80] constructed 'ultraflat' polynomials \(P_n(z)=\sum_{k \leq n} a_kz^k\) with \(\lvert a_k\rvert=1\) such that \(P_n(z)=(1+o(1))\sqrt{n}\) uniformly for all \(z\in\mathbb{C}\) with \(\lvert z\rvert=1\).

theorem erdos_230.variants.ultraflat : ∃ a : (n : ℕ) → Fin n → ℂ, (∀ n k, ‖a n k‖ = 1) ∧
    Tendsto (fun n : ℕ => ⨆ z : Metric.sphere (0 : ℂ) 1,
      |‖∑ k : Fin n, a n k * (z : ℂ) ^ ((k : ℕ) + 1)‖ / √n - 1|) atTop (𝓝 0)

Category research solved; AMS 30 Functions of a complex variable, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/230.lean, line 87.

Sources
LeanErdos230.erdos_230 · Erdos230.erdos_230.variants.ultraflat

TheoremErdős Problem 231#

References: - erdosproblems.com/231 - [Er57] Erdős, Paul, Some unsolved problems. Michigan Math. J. (1957), 291-300. - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Ke92] Keränen, Veikko, Abelian squares are avoidable on \(4\) letters. Automata, languages and programming (Vienna, 1992) (1992), 41-52. - [FiPu23] Fici, Gabriele and Puzynina, Svetlana, Abelian combinatorics on words: a survey. Comput. Sci. Rev. (2023), Paper No. 100532, 21.

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

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

Erdos231.erdos_231

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

Let \(S\) be a string of length \(2^k-1\) formed from an alphabet of \(k\) characters. Must \(S\) contain an abelian square: two consecutive blocks \(x\) and \(y\) such that \(y\) is a permutation of \(x\)?

Erdős initially conjectured that the answer is yes for all \(k\geq 2\), but for \(k=4\) this was disproved by de Bruijn and Erdős. Erdős then asked if there is in fact an infinite string formed from \(\{1,2,3,4\}\) which contains no abelian squares? This is equivalent to 192, and such a string was constructed by Keränen [Ke92]. The existence of this infinite string gives a negative answer to the problem for all \(k\geq 4\).

Containing no abelian squares is a stronger property than being squarefree (the existence of infinitely long squarefree strings over alphabets with \(k\geq 3\) characters was established by Thue). We refer to a recent survey by Fici and Puzynina [FiPu23] for more background and related results.

As stated, the answer is negative for every \(k \geq 2\): the strings \(121\) and \(1213121\) of length \(2^k - 1\) for \(k = 2, 3\) contain no abelian square. See erdos_231.variants.two_pow for strings of length \(2^k\).

theorem erdos_231 :
    ¬ ∀ k : ℕ, 2 ≤ k → ∀ S : List (Fin k), S.length = 2 ^ k - 1 → ContainsAbelianSquare S

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

Erdos231.erdos_231.variants.two_pow

Proved here.

Perhaps Erdős meant \(2^k\), where indeed there is an example for \(k=4\):

\[1213121412132124.\]

Every string of length \(2^k\) over \(k\) characters contains an abelian square for \(k = 2, 3\), but not for \(k \geq 4\).

theorem erdos_231.variants.two_pow :
    ¬ ∀ k : ℕ, 2 ≤ k → ∀ S : List (Fin k), S.length = 2 ^ k → ContainsAbelianSquare S

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

Erdos231.erdos_231.variants.two_pow_small

Proved here.

Every string of length \(2^k\) over \(k\) characters contains an abelian square for \(k = 2, 3\).

theorem erdos_231.variants.two_pow_small (k : ℕ) (hk : k = 2 ∨ k = 3) (S : List (Fin k))
    (hS : S.length = 2 ^ k) : ContainsAbelianSquare S

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

Sources
LeanErdos231.erdos_231 · Erdos231.erdos_231.variants.two_pow · Erdos231.erdos_231.variants.two_pow_small

TheoremErdős Problem 232#

References: - erdosproblems.com/232 - [ACMVZ23] Ambrus, Gergely and Csiszárik, Adrián and Matolcsi, Máté and Varga, Dániel and Zsámboki, Pál, The density of planar sets avoiding unit distances. Math. Program. (2023), arXiv:2207.14179. - [Cr67] Croft, H. T., Incidence incidents. Eureka (1967), 22-26. - [Er85] Erdős, Paul, Problems and results in combinatorial geometry. Discrete geometry and convexity (New York, 1982), Ann. New York Acad. Sci. 440 (1985), 1-11. PDF - [Mo66] Moser, L., Poorly formulated unsolved problems of combinatorial geometry. Mimeographed (1966).

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

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

Erdos232.erdos_232

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

For \(A\subset \mathbb{R}^2\) we define the upper density as

\[\overline{\delta}(A)=\limsup_{R\to \infty}\frac{\lambda(A \cap B_R)}{\lambda(B_R)},\]

where \(\lambda\) is the Lebesgue measure and \(B_R\) is the ball of radius \(R\).

Estimate

\[m_1=\sup \overline{\delta}(A),\]

where \(A\) ranges over all measurable subsets of \(\mathbb{R}^2\) without two points distance \(1\) apart. In particular, is \(m_1\leq 1/4\)?

A question of Moser [Mo66]; Erdős [Er85] conjectured \(m_1<1/4\). The answer is yes: Ambrus, Csiszárik, Matolcsi, Varga, and Zsámboki [ACMVZ23] proved that \(m_1\leq 0.247\).

theorem erdos_232 : m₁ ≤ 1 / 4

Category research solved; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/232.lean, line 79.

Erdos232.erdos_232.variants.acmvz_set

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

Ambrus, Csiszárik, Matolcsi, Varga, and Zsámboki [ACMVZ23, Theorem 1]: any Lebesgue measurable, \(1\)-avoiding planar set has upper density at most \(0.2470\).

theorem erdos_232.variants.acmvz_set (A : Set ℝ²) (hA : NullMeasurableSet A volume)
    (hfree : Erdos214.UnitDistanceAvoiding A) : upperDensity A ≤ 247 / 1000

Category research solved; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/232.lean, line 89.

Erdos232.erdos_232.variants.acmvz

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

Ambrus, Csiszárik, Matolcsi, Varga, and Zsámboki [ACMVZ23] proved that \(m_1\leq 0.247\).

theorem erdos_232.variants.acmvz : m₁ ≤ 247 / 1000

Category research solved; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/232.lean, line 99.

Erdos232.erdos_232.variants.hexagonal_lower_bound

Solved: stated here without proof.

A lower bound of \(m_1\geq \pi/(8\sqrt{3})\approx 0.2267\) is given by taking the union of open circular discs of radius \(1/2\) at a regular hexagonal lattice suitably spaced apart (see [ACMVZ23, Section 1]).

theorem erdos_232.variants.hexagonal_lower_bound :
    Real.pi / (8 * Real.sqrt 3) ≤ m₁

Category research solved; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/232.lean, line 108.

Erdos232.erdos_232.variants.croft_lower_bound

Solved: stated here without proof.

Croft [Cr67] gives a small improvement of \(m_1\geq 0.22936\) (see [ACMVZ23, Section 1]).

theorem erdos_232.variants.croft_lower_bound : 0.22936 ≤ m₁

Category research solved; AMS 28 Measure and integration, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/232.lean, line 116.

Sources
LeanErdos232.erdos_232 · Erdos232.erdos_232.variants.acmvz_set · Erdos232.erdos_232.variants.acmvz · Erdos232.erdos_232.variants.hexagonal_lower_bound · Erdos232.erdos_232.variants.croft_lower_bound

TheoremErdős Problem 233#

References: - erdosproblems.com/233 - A74741 - Wikipedia

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

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

Erdos233.erdos_233

Open: stated without proof.

A conjecture by Heath-Brown: The sum of squares of the first \(N\) gaps between consecutive primes behaves like \(N * (log N)^2\).

theorem erdos_233 :
    (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ)) =O[atTop] fun N => N * (log N)^2

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

Erdos233.erdos_233.variants.upper_bound

Solved: stated here without proof.

Cramér proved an upper bound of \(O(N(\log N)^4)\) conditional on the Riemann hypothesis.

theorem erdos_233.variants.upper_bound (h : RiemannHypothesis) :
    (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ)) =O[atTop] fun N => N * (log N)^4

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

Erdos233.erdos_233.variants.lower_bound

Solved: stated here; a Lean proof is at https://github.com/mzhorvath1/formal-conjectures/blob/032848c62fdf4c422bb0ee6663dc8d009d456c2c/FormalConjectures/ErdosProblems/233.lean#L57.

The prime number theorem immediately implies a lower bound of \(\gg N(\log N)^2\) for the sum of squares of gaps between consecutive primes.

Formal proof linked here provided by AlphaProof.

theorem erdos_233.variants.lower_bound :
    (fun (N : ℕ) => N * (log N)^2) =O[atTop]
    (fun N => ((∑ n ∈ Finset.range N, (primeGap n) ^ 2) : ℝ))

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

Sources
LeanErdos233.erdos_233 · Erdos233.erdos_233.variants.upper_bound · Erdos233.erdos_233.variants.lower_bound

TheoremErdős Problem 234#

Reference: erdosproblems.com/234

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

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

Erdos234.erdos_234

Open: stated without proof.

Is it true that for all c ≥ 0, the density f c of integers for which (p (n + 1) - p n) / log n < c exists and is a continuous function of c?

theorem erdos_234 : ∃ f : ℝ≥0 → ℝ, Continuous f ∧
    ∀ c : ℝ≥0, HasDensity {n : ℕ | primeGap n / log n < c} (f c)

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

Sources
LeanErdos234.erdos_234

TheoremErdős Problem 235#

References: - erdosproblems.com/235 - [Ho65] Hooley, Christopher, On the difference between consecutive numbers prime to \(n\). II. Publ. Math. Debrecen (1965), 39--49.

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

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

Erdos235.erdos_235

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

Let \(N_k=2\cdot 3\cdots p_k\) and \(\{a_1\lt a_2\lt \cdots \lt a_{\phi(N_k)}\}\) be the integers \(\lt N_k\) which are relatively prime to \(N_k\). Then, for any \(c\geq 0\), the limit

\[\frac{\#\{ a_i-a_{i-1}\leq c \frac{N_k}{\phi(N_k)} : 2\leq i\leq \phi(N_k)\}}{\phi(N_k)}\]

exists and is a continuous function of \(c\).

Solved by Hooley [Ho65], who proved that these gaps have an exponential distribution: that is, if \(f(c)\) is the function in question, then

\[f(c)=(1+o(1))(1-e^{-c})\]

(where the \(o(1)\) goes to \(0\) uniformly as \(k\to \infty\)).

See also 234 for a more difficult version of this problem using actual primes.

theorem erdos_235 :
    ∃ f : ℝ → ℝ, ContinuousOn f (Set.Ici (0 : ℝ)) ∧
      ∀ c, 0 ≤ c → Tendsto (fun k ↦ proportion k c) atTop (𝓝 (f c))

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

Erdos235.erdos_235.variants.hooley

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

Hooley [Ho65] proved that the limit in erdos_235 is \(1-e^{-c}\). For each fixed \(c\geq 0\),

\[f(c)=(1+o(1))(1-e^{-c})\]

as \(k\to\infty\).

theorem erdos_235.variants.hooley (c : ℝ) (hc : 0 ≤ c) :
    Tendsto (fun k ↦ proportion k c) atTop (𝓝 (1 - Real.exp (-c)))

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

Sources
LeanErdos235.erdos_235 · Erdos235.erdos_235.variants.hooley

TheoremErdős Problem 236#

Reference: erdosproblems.com/236

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

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

Erdos236.erdos_236

Open: stated without proof.

Let \(f(n)\) count the number of solutions to \(n=p+2^k\) for prime \(p\) and \(k\geq 0\). Show that \(f(n)=o(\log n)\).

theorem erdos_236: (fun n => (f n : ℝ)) =o[atTop] (fun n => Real.log (n : ℝ))

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

Sources
LeanErdos236.erdos_236

TheoremErdős Problem 237#

References: - erdosproblems.com/237 - [ChDi22] Chen, Y.-G. and Ding, Y., On a conjecture of Erdős. arXiv:2201.10727 (2022). - [Er50] Erdős, P., On integers of the form \(2^k+p\) and some related problems. Summa Brasil. Math. (1950), 113-123.

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

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

Erdos237.erdos_237

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

Let \(A\subseteq \mathbb{N}\) be a set such that \(\lvert A\cap \{1,\ldots,N\}\rvert \gg \log N\) for all large \(N\). Let \(f(n)\) count the number of solutions to \(n=p+a\) for \(p\) prime and \(a\in A\). Is it true that \(\limsup f(n)=\infty\)?

The answer is yes, as proved by Chen and Ding [ChDi22].

Here A may contain \(0\). This changes each \(f(n)\) by at most one, so it does not affect the answer.

theorem erdos_237 : ∀ A : Set ℕ,
    (fun N : ℕ ↦ Real.log N) =O[atTop] (fun N ↦ ((A ∩ .Icc 1 N).ncard : ℝ)) →
    limsup (fun n ↦ (f A n : ℕ∞)) atTop = ⊤

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

Erdos237.erdos_237.variants.infinite

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

Chen and Ding [ChDi22] proved that the assumption \(\lvert A\cap \{1,\ldots,N\}\rvert \gg \log N\) can be replaced with the assumption that \(A\) is infinite.

theorem erdos_237.variants.infinite (A : Set ℕ) (hA : A.Infinite) :
    limsup (fun n ↦ (f A n : ℕ∞)) atTop = ⊤

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

Erdos237.erdos_237.variants.pow_two

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

Erdős [Er50] proved the case \(A=\{2^k : k\geq 0\}\).

theorem erdos_237.variants.pow_two :
    limsup (fun n ↦ (f (Set.range (2 ^ ·)) n : ℕ∞)) atTop = ⊤

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

Sources
LeanErdos237.erdos_237 · Erdos237.erdos_237.variants.infinite · Erdos237.erdos_237.variants.pow_two

TheoremErdős Problem 238#

Reference: erdosproblems.com/238

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

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

Erdos238.erdos_238

Open: stated without proof.

Let c₁, c₂ > 0. Is it true that for any sufficiently large x, there exists more than c₁ * log x many consecutive primes ≤ x such that the difference between any two is > c₂?

theorem erdos_238 : ∀ᵉ (c₁ > 0) (c₂ > 0), ∀ᶠ (x : ℝ) in atTop, ∃ (k : ℕ),
    c₁ * log x < k ∧ ∃ f : Fin k → ℕ, ∃ m, (∀ i, f i ≤ x ∧ f i = (m + i.1).nth Nat.Prime)
    ∧ ∀ i : Fin (k - 1), c₂ < primeGap (m + i.1)

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

Erdos238.erdos_238.variants.small_c1

Solved: stated here without proof.

It is well-known that the conjecture above is true when c₁ is sufficiently small.

theorem erdos_238.variants.small_c1 : ∀ c₂ > 0, ∀ᶠ c₁ in 𝓝[>] 0, ∀ᶠ (x : ℝ) in atTop, ∃ (k : ℕ),
    c₁ * log x < k ∧ ∃ f : Fin k → ℕ, ∃ m, (∀ i, f i ≤ x ∧ f i = (m + i.1).nth Nat.Prime)
    ∧ ∀ i : Fin (k - 1), c₂ < primeGap (m + i.1)

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

Sources
LeanErdos238.erdos_238 · Erdos238.erdos_238.variants.small_c1

TheoremErdős Problem 239#

References: - erdosproblems.com/239 - [Ha68] Halász, G., Über die Mittelwerte multiplikativer zahlentheoretischer Funktionen. Acta Math. Acad. Sci. Hungar. (1968), 365-403. - [Wi67] Wirsing, E., Das asymptotische Verhalten von Summen über multiplikative Funk­tionen. Acta Math. Acad. Sei. Hung. (1967), 411-467.

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

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

Erdos239.erdos_239

Solved: stated here without proof.

Let \(f:\mathbb{N}\to \{-1,1\}\) be a multiplicative function. Is it true that

\[ \lim_{N\to \infty}\frac{1}{N}\sum_{n\leq N}f(n)\]

always exists?

The answer is yes, as proved by Wirsing [Wi67], and generalised by Halász [Ha68].

theorem erdos_239 :
    ∀ f : ℕ → ℝ,
    (∀ n ≥ 1, f n = 1 ∨ f n = -1) ∧
    (∀ m n, m.Coprime n → f (m * n) = f m * f n) ∧
    f 1 = 1 →
    ∃ L, Tendsto (fun N ↦ (∑ n ∈ Finset.Icc 1 N, f n) / N) atTop (𝓝 L)

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

Sources
LeanErdos239.erdos_239

TheoremErdős Problem 240#

References: - erdosproblems.com/240 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. PDF - [Po18] Pólya, Georg, Zur arithmetischen Untersuchung der Polynome. Math. Z. (1918), 143-148. - [Ti73] Tijdeman, R., On integers with many small prime factors. Compositio Math. 26 (1973), 319-330. numdam

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

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

Erdos240.erdos_240

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

Is there an infinite set of primes \(P\) such that if \(\{a_1\lt a_2\lt \cdots\}\) is the set of integers divisible only by primes in \(P\) then \(\lim a_{i+1}-a_i=\infty\)?

The answer is yes, proved by Tijdeman [Ti73, Theorem 7]. The question was asked to Erdős by Wintner [Er65b, p. 218]. See also Erdős Problem 368.

theorem erdos_240 :
    ∃ P : Set ℕ, P.Infinite ∧ P ⊆ {p : ℕ | p.Prime} ∧
      Tendsto (fun i ↦ a P (i + 1) - a P i) atTop atTop

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

Erdos240.erdos_240.variants.tijdeman_epsilon

Solved: stated here without proof.

Tijdeman [Ti73] resolved this question, proving that, for any \(\epsilon>0\), there exists an infinite set of primes \(P\) such that, with \(a_i\) defined as above,

\[a_{i+1}-a_i \gg a_i^{1-\epsilon}.\]

([Ti73, Theorem 7] is stated for \(0\lt \epsilon<1\); for \(\epsilon\geq 1\) the bound is trivial.)

theorem erdos_240.variants.tijdeman_epsilon (ε : ℝ) (hε : 0 < ε) :
    ∃ P : Set ℕ, P.Infinite ∧ P ⊆ {p : ℕ | p.Prime} ∧
      (fun i ↦ (a P i : ℝ) ^ (1 - ε)) =O[atTop] (fun i ↦ ((a P (i + 1) - a P i : ℕ) : ℝ))

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

Erdos240.erdos_240.variants.finite

Solved: stated here without proof.

The limit is infinite for a finite set of primes, which follows from a theorem of Pólya [Po18], that if \(f(n)\) is a quadratic integer polynomial without repeated roots then as \(n\to \infty\) the largest prime factor of \(f(n)\) also approaches infinity. Erdős [Er65b, p. 218] also credits this to Pólya.

Here \(P\) is nonempty: for \(P=\emptyset\) the set of integers is \(\{1\}\) and there are no gaps.

theorem erdos_240.variants.finite {P : Set ℕ} (hP : P.Finite) (hne : P.Nonempty)
    (hpr : P ⊆ {p : ℕ | p.Prime}) :
    Tendsto (fun i ↦ a P (i + 1) - a P i) atTop atTop

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

Erdos240.erdos_240.variants.tijdeman_finite

Solved: stated here without proof.

Tijdeman [Ti73] proved that, if \(P\) is a finite set of primes, then

\[a_{i+1}-a_i \gg \frac{a_i}{(\log a_i)^C}\]

for some constant \(C>0\) depending on \(P\).

[Ti73, Theorem 1 and its Corollary] state this for the integers composed of all primes at most \(p\); it follows for every finite set of primes, since a subset of these integers has larger gaps.

theorem erdos_240.variants.tijdeman_finite {P : Set ℕ} (hP : P.Finite) (hne : P.Nonempty)
    (hpr : P ⊆ {p : ℕ | p.Prime}) :
    ∃ C : ℝ, 0 < C ∧
      (fun i ↦ (a P i : ℝ) / Real.log (a P i : ℝ) ^ C) =O[atTop]
        (fun i ↦ ((a P (i + 1) - a P i : ℕ) : ℝ))

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

Sources
LeanErdos240.erdos_240 · Erdos240.erdos_240.variants.tijdeman_epsilon · Erdos240.erdos_240.variants.finite · Erdos240.erdos_240.variants.tijdeman_finite

TheoremErdős Problem 241#

References: - erdosproblems.com/30 - erdosproblems.com/241 - [BoCh62] Bose, R. C. and Chowla, S., Theorems in the additive theory of numbers. Comment. Math. Helv. (1962/63), 141-147. - [Gr01] Green, Ben, The number of squares and {\(B_h[g]\)} sets. Acta Arith. (2001), 365-390. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [Wh24] White, Ethan Patrick, An optimal \(L^2\) autoconvolution inequality. Canad. Math. Bull. 67 (2024), 108-121. doi:10.4153/S0008439523000565

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

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

Erdos241.erdos_241

Open: stated without proof.

Is it true that \(f(N)\sim N^{1/3}\)?

Originally asked to Erdős by Bose.

This is discussed in problem C11 of Guy's collection [Gu04].

theorem erdos_241 :
    (fun N ↦ (f N 3 : ℝ)) ~[atTop] (fun N ↦ (N : ℝ) ^ ((1 : ℝ) / 3))

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

Erdos241.erdos_241.variants.lower_bound

Solved: stated here without proof.

Bose and Chowla [BoCh62] provided a construction proving one half of this, namely \((1+o(1))N^{1/3}\leq f(N)\).

theorem erdos_241.variants.lower_bound :
    ∃ ε : ℕ → ℝ, ε =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ N in atTop, (1 + ε N) * (N : ℝ) ^ ((1 : ℝ) / 3) ≤ (f N 3 : ℝ)

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

Erdos241.erdos_241.variants.upper_bound

Solved: stated here without proof.

Green [Gr01] proved the upper bound \(f(N) \leq ((7/2)^{1/3}+o(1))N^{1/3}\) (note that \((7/2)^{1/3}\approx 1.519\)).

theorem erdos_241.variants.upper_bound :
    ∃ ε : ℕ → ℝ, ε =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ N in atTop, (f N 3 : ℝ) ≤ ((7 / 2 : ℝ) ^ ((1 : ℝ) / 3) + ε N) * (N : ℝ) ^ ((1 : ℝ) / 3)

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

Erdos241.erdos_241.variants.upper_bound_white

Solved: stated here without proof.

Green's argument gives \(f(N) \leq ((2/\mu_2^2)^{1/3}+o(1))N^{1/3}\), where \(\mu_2^2 = \inf \lVert g \ast g \rVert_2^2\) over \(g \colon [-1/2,1/2] \to \mathbb{R}\) with \(\int g = 1\); Green used \(\mu_2^2 \geq 4/7\). White [Wh24, Theorem 1 and Corollary 2] proved \(0.574636066 \leq \mu_2^2 \leq 0.574642912\), which gives the best upper bound known to date, \(f(N) \leq ((2/0.574636066)^{1/3}+o(1))N^{1/3}\) (note that \((2/0.574636066)^{1/3}\approx 1.5155\)).

theorem erdos_241.variants.upper_bound_white :
    ∃ ε : ℕ → ℝ, ε =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ N in atTop, (f N 3 : ℝ) ≤
      ((2 / 0.574636066 : ℝ) ^ ((1 : ℝ) / 3) + ε N) * (N : ℝ) ^ ((1 : ℝ) / 3)

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

Erdos241.erdos_241.variants.generalization

Open: stated without proof.

More generally, Bose and Chowla [BoCh62] conjectured that the maximum size of \(A\subseteq \{1,\ldots,N\}\) with all \(r\)-fold sums distinct (aside from the trivial coincidences) then \(\lvert A\rvert \sim N^{1/r}.\)

theorem erdos_241.variants.generalization (r : ℕ) (hr : r ≥ 2) :  BoseChowlaConjecture r

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

Erdos241.erdos_241.variants.r_eq_2

Solved: stated here without proof.

This is known only for \(r=2\) (see [erdosproblems.com/30]).

theorem erdos_241.variants.r_eq_2 :
    BoseChowlaConjecture 2

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

Sources
LeanErdos241.erdos_241 · Erdos241.erdos_241.variants.lower_bound · Erdos241.erdos_241.variants.upper_bound · Erdos241.erdos_241.variants.upper_bound_white · Erdos241.erdos_241.variants.generalization · Erdos241.erdos_241.variants.r_eq_2

TheoremErdős Problem 242#

References: - erdosproblems.com/242 - [Si56] Sierpiński, W., Sur les décompositions de nombres rationnels en fractions primaires. Mathesis (1956), 16--32.

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

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

Erdos242.erdos_242

Open: stated without proof.

For every \(n>2\) there exist distinct integers \(1 ≤ x < y < z\) such that \(\frac 4 n = \frac 1 x + \frac 1 y + \frac 1 z\).

theorem erdos_242 (n : ℕ) (hn : 2 < n) :
    ∃ x y z : ℕ, 1 ≤ x ∧ x < y ∧ y < z ∧
      (4 / n : ℚ) = 1 / x + 1 / y + 1 / z

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

Erdos242.erdos_242.variants.schinzel_generalization

Open: stated without proof.

Schinzel conjectured (see [Si56]) the generalisation that, for any fixed \(a\), if \(n\) is sufficiently large in terms of \(a\) then there exist distinct integers \(1\leq x < y < z\) such that \(\frac{a}{n} = \frac{1}{x}+\frac{1}{y}+\frac{1}{z}.\)

theorem erdos_242.variants.schinzel_generalization
    (a : ℕ) (ha : 0 < a) :
    ∀ᶠ (n : ℕ) in Filter.atTop, ∃ x y z : ℕ, 1 ≤ x ∧ x < y ∧ y < z ∧
      (a / n : ℚ) = 1 / x + 1 / y + 1 / z

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

Sources
LeanErdos242.erdos_242 · Erdos242.erdos_242.variants.schinzel_generalization

TheoremErdős Problem 243#

Reference: erdosproblems.com/243

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

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

Erdos243.erdos_243

Open: stated without proof.

Let \(a_1 < a_2 < \dots\) be a sequence of integers such that \(\lim_{n\to\infty} \frac{a_n}{a_{n-1}^2} = 1\) and \(\sum \frac{1}{a_n} \in \mathbb{Q}\).

Then, for all sufficiently large \(n \ge 1\), \(a_n = a_{n-1}^2 - a_{n-1} + 1\).

theorem erdos_243 (a : ℕ → ℕ) (ha₀ : StrictMono a)
    (ha₁ : Tendsto (fun n ↦ (a n : ℝ) / a (n - 1) ^ 2) atTop (𝓝 1))
    (ha₂ : Summable ((1 : ℚ) / a ·)) :
      ∀ᶠ n in atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

Category research open; AMS 40 Sequences, series, summability. Declared in FormalConjectures/ErdosProblems/243.lean, line 41.

Sources
LeanErdos243.erdos_243

TheoremErdős Problem 244#

Reference: erdosproblems.com/244

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

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

Erdos244.erdos_244

Open: stated without proof.

Let \(C > 1\). Does the set of integers of the form \(p + \lfloor C^k \rfloor\), for some prime \(p\) and \(k\geq 0\), have density \(>0\)?

theorem erdos_244 :
    ∀ C > (1 : ℝ), 0 < { p + ⌊C ^ k⌋₊ | (p) (k) (_ : p.Prime) }.lowerDensity

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

Erdos244.erdos_244.variants.Romanoff

Solved: stated here without proof.

Romanoff [Ro34] proved that the answer is yes if \(C\) is an integer.

[Ro34] Romanoff, N. P., Über einige Sätze der additiven Zahlentheorie. Math. Ann. (1934), 668-678.

theorem erdos_244.variants.Romanoff {C : ℕ} (hC : 1 < C) :
    0 < { p + ⌊C ^ k⌋₊ | (p) (k) (_ : p.Prime) }.lowerDensity

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

Sources
LeanErdos244.erdos_244 · Erdos244.erdos_244.variants.Romanoff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.