Erdős Problem 971 to Erdős Problem 996

TheoremErdős Problem 971#

Reference: erdosproblems.com/971

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

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

Erdos971.erdos_971

Open: stated without proof.

Let p(a, d) be the least prime congruent to a (mod d). Does there exist a constant c > 0 such that for all large d, p(a, d) > (1 + c) * φ(d) * log d for ≫ φ(d) many values of a?

theorem erdos_971 :
    ∃ c > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ d in atTop,
      C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) > (1 + c) * d.totient * log d}

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

Erdos971.erdos_971.variants.infinite_sequence

Solved: stated here without proof.

Erdős [Er49c] proved that the statement in erdos_971 holds for infinitely many values of d.

[Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

theorem erdos_971.variants.infinite_sequence :
    ∃ c > (0 : ℝ), ∃ C > (0 : ℝ),
      {d : ℕ | C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) > (1 + c) * d.totient * log d}}.Infinite

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

Erdos971.erdos_971.variants.many_small

Solved: stated here without proof.

Erdős [Er49c] proved that for any ε > 0 we have p(a, d) < ε * φ(d) * log d for ≫_ε φ(d) many values of a (for all large d).

[Er49c] Erdős, P., On some applications of Brun's method. Acta Univ. Szeged. Sect. Sci. Math. (1949), 57--63.

theorem erdos_971.variants.many_small :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ᶠ d in atTop,
      C * (d.totient : ℝ) ≤
        #{a < d | a.Coprime d ∧ (leastCongruentPrime a d : ℝ) < ε * d.totient * log d}

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

Sources

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

LeanErdos971.erdos_971 · Erdos971.erdos_971.variants.infinite_sequence · Erdos971.erdos_971.variants.many_small

TheoremErdős Problem 972#

Reference: erdosproblems.com/972

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

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

Erdos972.erdos_972

Open: stated without proof.

Erdős problem 972. Let \(\alpha > 1\) be irrational. Are there infinitely many primes \(p\) such that \(\lfloor p\alpha \rfloor\) is also prime?

theorem erdos_972 : ∀ α > 1, Irrational α → (primeSet α).Infinite

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

Sources

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

LeanErdos972.erdos_972

TheoremErdős Problem 973#

References: - erdosproblems.com/973 - [Er92f] Erdős, L., On some problems of {P}. Turán concerning power sums of complex numbers. Acta Math. Hungar. (1992), 11--24. - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180. - [LYZ26] Luo, Yanping and Yang, Ruiyi and Zhu, Keheng, Exterior power sums. arxiv/2607.22017 - [TWHC26] Tan, Xiaojun and Wang, Qihang and Huang, Wei and Chen, Kun, Residual bounds for Schur-stable polynomials. arxiv/2608.02043 - [Tu84b] Turán, Paul, On a new method of analysis and its applications. (1984), xvi+584. - PALOMAR-2026-09-20-000008

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

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

Erdos973.erdos_973

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/1571a487465fb6a87f92dcc46f1bd71b0846c413/erdos-973/Solution.lean#L47.

Does there exist a constant \(C>1\) such that, for every \(n\geq 2\), there exists a sequence \(z_i\in \mathbb{C}\) with \(z_1=1\) and \(\lvert z_i\rvert \geq 1\) for all \(1\leq i\leq n\) with \(\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert < C^{-n}\)?

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

The answer is no, by Luo, Yang and Zhu [LYZ26] (and via the residual-polynomial method of Tan, Wang, Huang and Chen [TWHC26]): the maximum exceeds \(e^{-\lambda n}\) for every fixed \(\lambda>0\) once \(n\) is large, so it decays subexponentially and no such \(C\) exists. See erdos_973.variants.luo_yang_zhu below.

theorem erdos_973 :
    ¬ ∃ C : ℝ, C > 1 ∧
      ∀ n : ℕ, n ≥ 2 → ∃ z : ℕ → ℂ,
        z 1 = 1 ∧
        (∀ i ∈ Icc 1 n, 1 ≤ ‖z i‖) ∧
        (∀ k ∈ Icc 2 (n + 1), ‖∑ i ∈ Icc 1 n, z i ^ k‖ < C ^ (-(n : ℝ)))

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

Erdos973.erdos_973.variants.luo_yang_zhu

Solved: stated here; a Lean proof is at https://github.com/linrock/math-proofs/blob/1571a487465fb6a87f92dcc46f1bd71b0846c413/erdos-973/Solution.lean#L53.

The result of [LYZ26] that settles the problem: for every fixed \(\lambda>0\) and all large enough \(n\), any \(z_1,\dots,z_n\) with \(\lvert z_j\rvert\geq 1\) satisfy \(\max_{2\leq k\leq n+1}\left\lvert\sum_j z_j^k\right\rvert > e^{-\lambda n}\).

This is sharper than erdos_973.variants.tang, whose bound \((2e)^{-(1+o(1))n}\) pins the rate at \(\log(2e) = 1 + \log 2\), still exponential decay.

theorem erdos_973.variants.luo_yang_zhu (lam : ℝ) (hlam : 0 < lam) :
    ∀ᶠ n in atTop, ∀ z : ℕ → ℂ,
      (∀ i ∈ Icc 1 n, 1 ≤ ‖z i‖) →
      ∃ k ∈ Icc 2 (n + 1),
        Real.exp (-lam * n) < ‖∑ i ∈ Icc 1 n, z i ^ k‖

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

Erdos973.erdos_973.variants.le_one

Solved: stated here without proof.

Erdős proved (as described on p.35 of [Tu84b]) that such a sequence does exist with \(\lvert z_i\rvert\leq 1\). Indeed, Erdős' construction gives a value of \(C\approx 1.32\).

theorem erdos_973.variants.le_one :
    ∃ C : ℝ, C > 1 ∧
      ∀ n : ℕ, n ≥ 2 → ∃ z : ℕ → ℂ,
        z 1 = 1 ∧
        (∀ i ∈ Icc 1 n, ‖z i‖ ≤ 1) ∧
        (∀ k ∈ Icc 2 (n + 1), ‖∑ i ∈ Icc 1 n, z i ^ k‖ < C ^ (-(n : ℝ)))

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

Erdos973.erdos_973.variants.m2_bounds

Solved: stated here without proof.

In [Er92f] (a different) Erdős refines this analysis, proving that if \(M_2=\min_{z_j} \max_{2\leq k\leq n+1} \left\lvert \sum_{1\leq j\leq n}z_j^k\right\rvert\) where the minimum is taken over all \(z_j\in \mathbb{C}\) with \(\max \lvert z_j\rvert=1\), then \((1.746)^{-n} < M_2 < (1.745)^{-n}\) for all sufficiently large \(n\).

theorem erdos_973.variants.m2_bounds :
    ∀ᶠ n : ℕ in atTop, ∀ M_2 : ℝ,
      IsGLB { M | ∃ z : ℕ → ℂ,
        (∀ j ∈ Icc 1 n, ‖z j‖ ≤ 1) ∧
        (∃ j ∈ Icc 1 n, ‖z j‖ = 1) ∧
        (∃ k ∈ Icc 2 (n + 1), M = ‖∑ j ∈ Icc 1 n, z j ^ k‖ ∧
          ∀ m ∈ Icc 2 (n + 1), ‖∑ j ∈ Icc 1 n, z j ^ m‖ ≤ M) } M_2 →
      (1.746 : ℝ) ^ (-(n : ℝ)) < M_2 ∧ M_2 < (1.745 : ℝ) ^ (-(n : ℝ))

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

Erdos973.erdos_973.variants.tang

Solved: stated here without proof.

Tang notes in the comments that Theorem 6.1 of [Tu84b] implies that, if \(\lvert z_i\rvert \geq 1\) for all \(i\), then \(\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert \geq (2e)^{-(1+o(1))n}\).

theorem erdos_973.variants.tang :
    ∃ f : ℕ → ℝ, f =o[atTop] (fun _ ↦ (1 : ℝ)) ∧
    ∀ᶠ n in atTop, ∀ z : ℕ → ℂ,
      (∀ i ∈ Icc 1 n, 1 ≤ ‖z i‖) →
      ∃ k ∈ Icc 2 (n + 1),
        ‖∑ i ∈ Icc 1 n, z i ^ k‖ ≥
        (2 * Real.exp 1) ^ (-(1 + f n) * (n : ℝ))

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

Sources

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

LeanErdos973.erdos_973 · Erdos973.erdos_973.variants.luo_yang_zhu · Erdos973.erdos_973.variants.le_one · Erdos973.erdos_973.variants.m2_bounds · Erdos973.erdos_973.variants.tang

TheoremErdős Problem 974#

References: - erdosproblems.com/974 - [Ti66] Tijdeman, R., On a conjecture of Turán and Erdős. Indag. Math. (1966), 374-383.

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

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

Erdos974.erdos_974

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

Let \(z_1,\ldots,z_n\in \mathbb{C}\) be a sequence such that \(z_1=1\). Suppose that the sequence of

\[s_k=\sum_{1\leq i\leq n}z_i^k\]

contains infinitely many \((n-1)\)-tuples of consecutive values of \(s_k\) which are all \(0\). Then (essentially)

\[z_j=e(j/n),\]

where \(e(x)=e^{2\pi ix}\).

A conjecture of Turán.

This is true (in the stronger form with only two such tuples) - in fact if \(n\) is odd then the \(z_i\) must be exactly the \(n\)th roots of unity, and if \(n\) is even they must be the vertices of two regular \((n/2)\)-gons with the same circumscribed circle centred at the origin. This was first proved by Tijdeman [Ti66]. An independent proof of this was given in the comments section by Hu, Tang, and Zhang.

theorem erdos_974 {n : ℕ} [NeZero n] (z : Fin n → ℂ) (hz : z 0 = 1)
    (hs : Set.Infinite {k : ℕ | ∀ j < n - 1, ∑ i, z i ^ (k + j) = 0}) :
    IsTuranConfiguration z

Category research solved; AMS 11 Number theory, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/974.lean, line 61.

Erdos974.erdos_974.variants.two_tuples

Solved: stated here without proof.

Erdős speculates that this may be true if there are two distinct \((n-1)\)-tuples of consecutive values of \(s_k\) which are \(0\). He does not elaborate on what the 'essentially' may mean precisely.

This is true (in the stronger form with only two such tuples) - in fact if \(n\) is odd then the \(z_i\) must be exactly the \(n\)th roots of unity, and if \(n\) is even they must be the vertices of two regular \((n/2)\)-gons with the same circumscribed circle centred at the origin. This was first proved by Tijdeman [Ti66]. An independent proof of this was given in the comments section by Hu, Tang, and Zhang.

theorem erdos_974.variants.two_tuples {n : ℕ} [NeZero n] (z : Fin n → ℂ) (hz : z 0 = 1)
    {a b : ℕ} (hab : a ≠ b) (ha : ∀ j < n - 1, ∑ i, z i ^ (a + j) = 0)
    (hb : ∀ j < n - 1, ∑ i, z i ^ (b + j) = 0) :
    IsTuranConfiguration z

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

Sources

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

LeanErdos974.erdos_974 · Erdos974.erdos_974.variants.two_tuples

TheoremErdős Problem 975#

References: - erdosproblems.com/975 - [Va39] van der Corput, J. G., Une in\'egalit\'e{} relative au nombre des diviseurs. Nederl. Akad. Wetensch., Proc. (1939), 547--553. - [Er52b] Erd\"os, P., On the sum {\(\sum^x_{k=1} d(f(k))\)}. J. London Math. Soc. (1952), 7--15. - [Ho63] Hooley, Christopher, On the number of divisors of a quadratic polynomial. Acta Math. (1963), 97--114. - [Mc95] McKee, James, On the average number of divisors of quadratic polynomials. Math. Proc. Cambridge Philos. Soc. (1995), 389--392. - [Mc97] McKee, James, A note on the number of divisors of quadratic polynomials. (1997), 275--281. - [Mc99] McKee, James, The average number of divisors of an irreducible quadratic polynomial. Math. Proc. Cambridge Philos. Soc. (1999), 17--22. - [T] T. Tao, Erdos' divisor bound, https://terrytao.wordpress.com/2011/07/23/erdos-divisor-bound/

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

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

Erdos975.erdos_975

Open: stated without proof.

For an irreducible polynomial \(f \in \mathbb{Z}[x]\) with \(f(n) \ge 1\) for sufficiently large \(n\), does there exists a constant \(c = c(f) > 0\) such that \(\sum_{n \le x} \tau(f(n)) \approx c \cdot x \log x\)?

Note that it is unclear whether the polynomial should have integer coefficients or merely be integer-valued. We assume the former.

theorem erdos_975 :
    ∀ f : ℤ[X], f.natDegree ≠ 0 → Irreducible f → (∀ᶠ n in atTop, 1 ≤ f.eval n) →
    ∃ c > (0 : ℝ), Tendsto (fun x ↦ Erdos975Sum f x / (x * log x)) atTop (𝓝 c)

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

Erdos975.erdos_975.variants.upper_bound

Solved: stated here without proof.

The correctness of the growth rate is shown in [Va39] (lower bound) and [Er52b] (upper bound).

theorem erdos_975.variants.upper_bound (f : ℤ[X]) (hf : Irreducible f)
    (hf_pos : ∀ᶠ n in atTop, 1 ≤ f.eval n) : Erdos975Sum f =O[atTop] (fun x ↦ x * log x)

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

Erdos975.erdos_975.variants.lower_bound

Solved: stated here without proof.

Lower bound for the growth rate of Erdos975Sum, shown in [Va39].

theorem erdos_975.variants.lower_bound (f : ℤ[X]) (hf : Irreducible f) (hfdeg : f.natDegree ≠ 0)
    (hf_pos : ∀ᶠ n in atTop, 1 ≤ f.eval n) :
    (fun x ↦ x * log x) =O[atTop] Erdos975Sum f

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

Erdos975.erdos_975.variants.quadratic

Solved: stated here without proof.

When \(f\) is an irreducible quadratic polynomial, the question is answered first by Hooley [Ho63]. More compact expression of the constant in terms of Hurwitz class numbers (when \(a = 1\)) is given by McKey in [Mc95], [Mc97], [Mc99].

TODO: formalize Hurwitz class numbers and the expression of the constant in terms of them.

theorem erdos_975.variants.quadratic (f : ℤ[X]) (hf : Irreducible f)
    (hf_pos : ∀ᶠ n : ℕ in atTop, 1 ≤ f.eval ↑n) (hf_degree : f.degree = 2) (c : ℝ) :
    c = erdos_975.variants.quadratic.answer → 0 < c ∧ Tendsto
      (fun x ↦ Erdos975Sum f x / (x * log x)) atTop (𝓝 c)

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

Erdos975.erdos_975.variants.n2_plus_1_strong

Solved: stated here without proof.

More concrete example for \(f(n) = n^2 + 1\), where the asymptote is \(\sum_{n \le x} \tau(n^2 + 1) \sim \frac{3}{\pi} x \log x + O(x)\). See Tao's blog [T].

theorem erdos_975.variants.n2_plus_1_strong :
    (fun x ↦ Erdos975Sum (X ^ 2 + 1) x - (3 / π) * x * log x) =O[atTop] id

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

Erdos975.erdos_975.variants.n2_plus_1

Solved: stated here without proof.

Asymptotics for Erdos975Sum with \(f(X) = X^2 + 1\).

theorem erdos_975.variants.n2_plus_1 :
    ∃ c > (0 : ℝ), Tendsto (fun x ↦ Erdos975Sum (X ^ 2 + 1) x / (x * log x)) atTop (𝓝 c)

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

Sources

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

LeanErdos975.erdos_975 · Erdos975.erdos_975.variants.upper_bound · Erdos975.erdos_975.variants.lower_bound · Erdos975.erdos_975.variants.quadratic · Erdos975.erdos_975.variants.n2_plus_1_strong · Erdos975.erdos_975.variants.n2_plus_1

TheoremErdős Problem 976#

References: - erdosproblems.com/976 - [Er52c] Erdős, P., On the greatest prime factor of \(\prod_{k=1}^x f(k)\). J. London Math. Soc. 27 (1952), 379-384. - [Er65b] Erdős, P., Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Na22] Nagell, T., Abh. Math. Sem. Hamburg 1 (1922), 179-194. - [Ri34] Ricci, G., Annali di Mat. (1934), 295-303. - [Te90] Tenenbaum, G., Sur une question d'Erdős et Schinzel. A tribute to Paul Erdős (1990), 405-443.

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

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

Erdos976.erdos_976

Open: stated without proof.

Let \(f\in \mathbb{Z}[x]\) be an irreducible polynomial of degree \(d\geq 2\). Let \(F_f(n)\) be maximal such that there exists \(1\leq m\leq n\) with \(f(m)\) is divisible by a prime \(\geq F_f(n)\). Equivalently, \(F_f(n)\) is the greatest prime divisor of

\[\prod_{1\leq m\leq n}f(m).\]

Estimate \(F_f(n)\).

We read "estimate" as determining the order of magnitude of \(F_f(n)\).

theorem erdos_976 (f : ℤ[X]) (hf : Irreducible f) (hd : 2 ≤ f.natDegree) :
    (fun n ↦ (F f n : ℝ)) =Θ[atTop] erdos_976.answer f

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

Erdos976.erdos_976.parts.i

Open: stated without proof.

Let \(f\in \mathbb{Z}[x]\) be an irreducible polynomial of degree \(d\geq 2\), and let \(F_f(n)\) be the greatest prime divisor of \(\prod_{1\leq m\leq n}f(m)\). Is it true that \(F_f(n)\gg n^{1+c}\) for some constant \(c>0\)?

theorem erdos_976.parts.i :
    ∀ f : ℤ[X], Irreducible f → 2 ≤ f.natDegree →
      ∃ c > (0 : ℝ), (fun n : ℕ ↦ (n : ℝ) ^ (1 + c)) =O[atTop] fun n ↦ (F f n : ℝ)

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

Erdos976.erdos_976.parts.ii

Open: stated without proof.

Let \(f\in \mathbb{Z}[x]\) be an irreducible polynomial of degree \(d\geq 2\), and let \(F_f(n)\) be the greatest prime divisor of \(\prod_{1\leq m\leq n}f(m)\). Is it true that \(F_f(n)\gg n^d\)?

theorem erdos_976.parts.ii :
    ∀ f : ℤ[X], Irreducible f → 2 ≤ f.natDegree →
      (fun n : ℕ ↦ (n : ℝ) ^ f.natDegree) =O[atTop] fun n ↦ (F f n : ℝ)

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

Erdos976.erdos_976.variants.nagell_ricci

Solved: stated here without proof.

Nagell [Na22] and Ricci [Ri34] proved that \(F_f(n) \gg n\log n\).

theorem erdos_976.variants.nagell_ricci (f : ℤ[X]) (hf : Irreducible f)
    (hd : 2 ≤ f.natDegree) :
    (fun n : ℕ ↦ (n : ℝ) * Real.log n) =O[atTop] fun n ↦ (F f n : ℝ)

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

Erdos976.erdos_976.variants.erdos

Solved: stated here without proof.

Erdős [Er52c] improved the bound of Nagell and Ricci to

\[F_f(n) \gg n(\log n)^{\log\log\log n}.\]

More precisely, [Er52c] gives \(F_f(n) > n(\log n)^{c\log\log\log n}\) for some constant \(c = c(f) > 0\); the site omits \(c\).

theorem erdos_976.variants.erdos (f : ℤ[X]) (hf : Irreducible f) (hd : 2 ≤ f.natDegree) :
    ∃ c > (0 : ℝ),
      (fun n : ℕ ↦ (n : ℝ) * Real.log n ^ (c * Real.log (Real.log (Real.log n)))) =O[atTop]
        fun n ↦ (F f n : ℝ)

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

Erdos976.erdos_976.variants.tenenbaum

Solved: stated here without proof.

In [Er65b] Erdős claimed a proof of \(F_f(n) \gg n\exp((\log n)^c)\) for some constant \(c>0\), but never published it. A proof was provided by Tenenbaum [Te90].

theorem erdos_976.variants.tenenbaum (f : ℤ[X]) (hf : Irreducible f) (hd : 2 ≤ f.natDegree) :
    ∃ c > (0 : ℝ), (fun n : ℕ ↦ (n : ℝ) * Real.exp (Real.log n ^ c)) =O[atTop]
      fun n ↦ (F f n : ℝ)

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

Sources

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

LeanErdos976.erdos_976 · Erdos976.erdos_976.parts.i · Erdos976.erdos_976.parts.ii · Erdos976.erdos_976.variants.nagell_ricci · Erdos976.erdos_976.variants.erdos · Erdos976.erdos_976.variants.tenenbaum

TheoremErdős Problem 977#

References: - erdosproblems.com/977 - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Sc62] Schinzel, A., On primitive prime factors of \(a^n-b^n\). Proc. Cambridge Philos. Soc. (1962), 555-562. - [St74b] Stewart, C. L., The greatest prime factor of \(a^n-b^n\). Acta Arith. (1974/75), 427-433. - [St13] Stewart, Cameron L., On divisors of Lucas and Lehmer numbers. Acta Math. (2013), 291-314. - [MuWo02] Murty, Ram and Wong, Siman, The \(ABC\) conjecture and prime divisors of the Lucas and Lehmer sequences. (2002), 43-54. - [La21] L. Lai, On the largest prime divisor of \(n!+1\). arXiv:2103.14894 (2021).

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

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

Erdos977.erdos_977

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

If \(P(m)\) is the greatest prime divisor of \(m\), then is it true that

\[\frac{P(2^n-1)}{n}\to \infty\]

as \(n\to \infty\)?

Schinzel [Sc62] proved that \(P(2^n-1)>2n\) for \(n>12\). In [Er65b] Erdős also asks about \(P(n!+1)\). Stewart [St74b] proved that this conjecture is true if we restrict \(n\) to those integers with \(\lt \frac{1}{\log 2}\log\log n\) many prime factors.

This was proved in the affirmative by Stewart [St13], who proved that \(P(2^n-1)\gg n^{1+\frac{1}{104\log\log n}}\) for all large \(n\).

theorem erdos_977 :
    Tendsto (fun n : ℕ ↦ (Nat.maxPrimeFac (2 ^ n - 1) : ℝ) / n) atTop atTop

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

Erdos977.erdos_977.variants.schinzel

Solved: stated here without proof.

Schinzel [Sc62] proved that \(P(2^n-1)>2n\) for \(n>12\).

theorem erdos_977.variants.schinzel :
    ∀ n : ℕ, 12 < n → 2 * n < Nat.maxPrimeFac (2 ^ n - 1)

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

Erdos977.erdos_977.variants.stewart

Solved: stated here without proof.

Stewart [St13] proved that \(P(2^n-1)\gg n^{1+\frac{1}{104\log\log n}}\) for all large \(n\).

theorem erdos_977.variants.stewart : ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop,
    c * (n : ℝ) ^ (1 + 1 / (104 * Real.log (Real.log n))) ≤ Nat.maxPrimeFac (2 ^ n - 1)

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

Erdos977.erdos_977.variants.factorial

Open: stated without proof.

In [Er65b] Erdős also asks about \(P(n!+1)\): is it true that \(P(n!+1)/n\to\infty\)? This appears to be open still. Murty and Wong [MuWo02] proved that \(P(n!+1)>(1+o(1))n\log n\) assuming the abc conjecture.

theorem erdos_977.variants.factorial :
    Tendsto (fun n : ℕ ↦ (Nat.maxPrimeFac (n.factorial + 1) : ℝ) / n) atTop atTop

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

Erdos977.erdos_977.variants.lai

Solved: stated here without proof.

The best-known unconditional result, due to Lai [La21], is that

\[\limsup \frac{P(n!+1)}{n} \geq 1+9\log 2\approx 7.238.\]

theorem erdos_977.variants.lai : ∀ C : ℝ, C < 1 + 9 * Real.log 2 →
    ∃ᶠ n : ℕ in atTop, C * n < Nat.maxPrimeFac (n.factorial + 1)

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

Sources

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

LeanErdos977.erdos_977 · Erdos977.erdos_977.variants.schinzel · Erdos977.erdos_977.variants.stewart · Erdos977.erdos_977.variants.factorial · Erdos977.erdos_977.variants.lai

TheoremErdős Problem 978#

Reference: - erdosproblems.com/978 - [Ho67] Hooley, C., On the power free values of polynomials. Mathematika (1967), 21--26. - [Br11] Browning, T. D., Power-free values of polynomials. Arch. Math. (Basel) (2011), 139--150. - [Er53] Erdős, P., Arithmetical properties of polynomials. J. London Math. Soc. (1953), 416--425. - [OAI26a] OpenAI, Squarefree values of quartics and power-free values of polynomials. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Squarefree-values-of-quartics-and-power-free-values-of-polynomials-September-24-2026/manuscript.pdf

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

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

Erdos978.erdos_978.variants.sub_one

Solved: stated here without proof.

Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2 and is not equal to a power of 2. Then the set of n such that f n is (k - 1)-th power free is infinite, and this is proved in [Er53].

theorem erdos_978.variants.sub_one {f : ℤ[X]} (hi : Irreducible f) (hd : 2 < f.natDegree)
    (hp : ∀ (x : ℕ), f.natDegree ≠ 2 ^ x) (hlc : 0 < f.leadingCoeff) :
    {n : ℕ | Powerfree (f.natDegree - 1) (f.eval (n : ℤ))}.Infinite

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

Erdos978.erdos_978.parts.i

Solved: stated here without proof.

Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2, is not equal to a power of 2, and f n has no fixed (k - 1)-th power divisors other than 1. Then the set of n such that f n is (k - 1)-th power free has positive density, and this is proved in [Ho67].

theorem erdos_978.parts.i {f : ℤ[X]} (hi : Irreducible f) (hd : 2 < f.natDegree)
    (hp2 : ∀ (x : ℕ), f.natDegree ≠ 2 ^ x) (hlc : 0 < f.leadingCoeff)
    (hp : ∀ (p : ℕ), p.Prime → ∃ n : ℕ, ¬ (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) :
    HasPosDensity {n : ℕ | Powerfree (f.natDegree - 1) (f.eval (n : ℤ))}

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

Erdos978.erdos_978.variants.sub_two

Solved: stated here without proof.

If the degree k of f is larger than or equal to 9, and f n has no fixed (k - 2)-th power divisors other than 1, then the set of n such that f n is (k - 2)-th power free has infinitely many elements. This result is proved in [Br11].

theorem erdos_978.variants.sub_two {f : ℤ[X]} (hi : Irreducible f) (hd : 9 ≤ f.natDegree)
    (hp : ∀ (p : ℕ), p.Prime → ∃ n : ℕ, ¬ (p : ℤ) ^ (f.natDegree - 2) ∣ f.eval (n : ℤ)) :
    {n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite

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

Erdos978.erdos_978.variants.allow_fixed_divisors

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/3b5d6ac2555cd63b83d418c29ff040876be9dee0/FormalConjectures/ErdosProblems/978.lean#L64.

If \(k > 3\) (and \(k \neq 2^l\)), then are there infinitely many \(n\) for which \(f(n)\) is \((k-2)\)-power-free?

This was disproved by the DeepMind prover agent.

theorem erdos_978.variants.allow_fixed_divisors :
    ¬ ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 3 →
    (¬ ∃ l : ℕ, f.natDegree = 2 ^ l) → 0 < f.leadingCoeff →
    (¬ ∃ p : ℕ, p.Prime ∧ ∀ n : ℕ, (p : ℤ) ^ (f.natDegree - 1) ∣ f.eval (n : ℤ)) →
    {n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite

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

Erdos978.erdos_978.parts.ii

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PowerFree/Main.lean#L144.

If \(k>3\) (and \(k \neq 2^l\)), and for all primes \(p\) there exists \(n\) such that \(p^{k-2}\nmid f(n)\), then are there infinitely many \(n\) for which \(f(n)\) is \((k-2)\)-power-free?

This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which gives positive density and does not need \(k \neq 2^l\) or a positive leading coefficient.

theorem erdos_978.parts.ii :
    ∀ {f : ℤ[X]}, Irreducible f → f.natDegree > 3 →
    (¬ ∃ l : ℕ, f.natDegree = 2 ^ l) → 0 < f.leadingCoeff →
    (∀ (p : ℕ), p.Prime → ∃ n : ℕ, ¬ (p : ℤ) ^ (f.natDegree - 2) ∣ f.eval (n : ℤ)) →
    {n : ℕ | Powerfree (f.natDegree - 2) (f.eval (n : ℤ))}.Infinite

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

Erdos978.erdos_978.parts.iii

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PowerFree/Main.lean#L144.

Does n ^ 4 + 2 represent infinitely many squarefree numbers?

This was proved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof, which gives positive density for every irreducible quartic with no fixed square divisor.

theorem erdos_978.parts.iii : {n : ℕ | Squarefree (n ^ 4 + 2)}.Infinite

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

Sources

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

LeanErdos978.erdos_978.variants.sub_one · Erdos978.erdos_978.parts.i · Erdos978.erdos_978.variants.sub_two · Erdos978.erdos_978.variants.allow_fixed_divisors · Erdos978.erdos_978.parts.ii · Erdos978.erdos_978.parts.iii

TheoremErdős Problem 979#

Reference: erdosproblems.com/979

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

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

Erdos979.erdos_979

Open: stated without proof.

Let \(k ≥ 2\), and let \(f_k(n)\) count the number of solutions to \(n = p_1^k + \dots + p_k^k\), where the \(p_i\) are prime numbers. Is it true that \(\limsup f_k(n) = \infty\)?

theorem erdos_979 :
    ∀ k ≥ 2, Filter.limsup (fun n => (solutionSet n k).encard) Filter.atTop = ⊤

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

Erdos979.erdos_979.variants.k2

Solved: stated here without proof.

Erdős [Er37b] proved that if \(f_2(n)\) counts the number of solutions to \(n = p_1^2 + p_2^2\), where \(p_1\) and \(p_2\) are prime numbers, then \(\limsup f_2(n) = \infty\).

[Er37b] Erdős, Paul, On the Sum and Difference of Squares of Primes. J. London Math. Soc. (1937), 133--136.

theorem erdos_979.variants.k2 :
    Filter.limsup (fun n => (solutionSet n 2).encard) Filter.atTop = ⊤

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

Erdos979.erdos_979.variants.k3

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-979-k3/blob/930fcc877fa4a2b4fc7c59614cbbab04a6d834ca/lean/K3Lean/Erdos979K3Final.lean#L46-L47.

Erdős (unpublished)

theorem erdos_979.variants.k3 :
    Filter.limsup (fun n => (solutionSet n 3).encard) Filter.atTop = ⊤

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

Sources

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

LeanErdos979.erdos_979 · Erdos979.erdos_979.variants.k2 · Erdos979.erdos_979.variants.k3

TheoremErdős Problem 980#

References: - erdosproblems.com/980 - [El67b] Elliott, P. D. T. A., A problem of Erdős concerning power residue sums. Acta Arith. 13 (1967/68), 131-149. - [Er61e] Erdős, P., Remarks on number theory. I. Mat. Lapok (1961), 10-17. - [Er65b] Erdős, P., Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [MaPo11] Martin, G. and Pollack, P., The average least character nonresidue and further variations on a theme of Erdős. arXiv:1112.1175 (2011).

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

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

Erdos980.erdos_980

Solved: stated here without proof.

Let \(k\geq 2\) and \(n_k(p)\) denote the least \(k\)th power nonresidue of \(p\). Is it true that

\[\sum_{p\lt x} n_k(p)\sim c_k \frac{x}{\log x}\]

for some constant \(c_k>0\)?

Erdős [Er65b] asked this; it is true, and was proved by Elliott [El67b]. As in [El67b], the sum is over the primes \(p \equiv 1 \pmod k\) (for each of which a \(k\)th power nonresidue exists).

theorem erdos_980 (k : ℕ) (hk : 2 ≤ k) :
    ∃ c > (0 : ℝ), residueSum k ~[atTop] fun x ↦ c * x / Real.log x

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

Erdos980.erdos_980.variants.erdos_two

Solved: stated here without proof.

Erdős [Er61e] proved this when \(k=2\), with

\[c_2=\sum_{k=1}^\infty \frac{p_k}{2^k},\]

where \(p_k\) is the \(k\)th prime; the sum is over the odd primes \(p < x\) [MaPo11, (1.1)].

theorem erdos_980.variants.erdos_two :
    residueSum 2 ~[atTop]
      fun x ↦ (∑' i : ℕ, (Nat.nth Nat.Prime i : ℝ) / 2 ^ (i + 1)) * x / Real.log x

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

Sources

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

LeanErdos980.erdos_980 · Erdos980.erdos_980.variants.erdos_two

TheoremErdős Problem 981#

References: - erdosproblems.com/981 - [El69] Elliott, P. D. T. A., A conjecture of Erdős concerning character sums. Indag. Math. 31 (1969), 164–171. - [TaZh25] arxiv/2512.24631 Average first-passage times for character sums by Quanyu Tang and Hao Zhang

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

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

Erdos981.erdos_981

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

Let \(\epsilon > 0\) and \(f_\epsilon(p)\) be the smallest integer \(m\) such that \(\sum_{n\leq N} \left(\frac{n}{p}\right)\lt \epsilon N\) for all \(N\geq m\). Prove that

\[\sum_{p\lt x}f_\epsilon(p)\sim c_\epsilon \frac{x}{\log x}\]

for some \(c_\epsilon > 0\).

Proved by Elliott [El69].

theorem erdos_981 (ε : ℝ) (hε : 0 < ε) :
    ∃ c > (0 : ℝ), Tendsto (fun x ↦ (∑ p : Nat.primesBelow ⌈x⌉₊, f ε p) * log x / x) atTop (𝓝 c)

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

Erdos981.erdos_981.variants.first_time

Solved: stated here without proof.

Let \(\epsilon > 0\) and \(f_\epsilon(p)\) be the smallest integer \(m\) such that \(\sum_{n\leq m} \left(\frac{n}{p}\right)\lt \epsilon m\). Prove that

\[\sum_{p\lt x}f_\epsilon(p)\sim c_\epsilon \frac{x}{\log x}\]

for some \(c_\epsilon > 0\).

Proved by Tang and Zhang [TaZh25].

theorem erdos_981.variants.first_time (ε : ℝ) (hε : 0 < ε) :
    ∃ c > (0 : ℝ), Tendsto (fun x ↦ (∑ p : Nat.primesBelow ⌈x⌉₊, f' ε p) * log x / x) atTop (𝓝 c)

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

Sources

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

LeanErdos981.erdos_981 · Erdos981.erdos_981.variants.first_time

TheoremErdős Problem 982#

Reference: erdosproblems.com/982

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

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

Erdos982.erdos_982

Open: stated without proof.

If \(n\) distinct points in \(\mathbb{R}^2\) form a convex polygon then some vertex has at least \(\lfloor\frac{n}{2}\rfloor\) different distances to other vertices.

theorem erdos_982 (n : ℕ) (hn : 3 ≤ n) (p : Fin n → ℝ²) (hp : Function.Injective p)
    (hp' : EuclideanGeometry.IsConvexPolygon p) :
    ∃ (i : Fin n), { d : ℝ | ∃ j : Fin n, j ≠ i ∧ d = dist (p i) (p j) }.ncard ≥ n / 2

Category research open; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/982.lean, line 37.

Erdos982.erdos_982.variants.concyclic

Solved: stated here; a Lean proof is at https://github.com/arex1337/formal-conjectures-proofs/blob/3b7d581c75fd00e482deabfb20675cf3ccfaf49f/Erdos982/GeneralCircle.lean.

For distinct points on a common circle, every vertex has at least \(\lfloor\frac{n}{2}\rfloor\) different distances to the other vertices. This does not require convexity or the assumption \(3 \leq n\).

theorem erdos_982.variants.concyclic {n : ℕ} (p : Fin n → ℝ²) (hp : Function.Injective p)
    (c : ℝ²) (R : ℝ) (hR : ∀ j, dist (p j) c = R) (i : Fin n) :
    { d : ℝ | ∃ j : Fin n, j ≠ i ∧ d = dist (p i) (p j) }.ncard ≥ n / 2

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

Sources

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

LeanErdos982.erdos_982 · Erdos982.erdos_982.variants.concyclic

TheoremErdős Problem 983#

References: - erdosproblems.com/983 - [Er70b] Erdős, P., Some applications of graph theory to number theory. Proc. Second Chapel Hill Conf. on Combinatorial Mathematics and its Applications (Univ. North Carolina, Chapel Hill, N.C., 1970) (1970), 136-145. PDF - [Po79] Pomerance, C., The prime number graph. Math. Comp. 33 (1979), 399-408. PDF

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

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

Erdos983.erdos_983.parts.i

Solved: stated here without proof.

Let \(n\geq 2\) and \(\pi(n)\lt k\leq n\). Let \(f(k,n)\) be the smallest integer \(r\) such that in any \(A\subseteq \{1,\ldots,n\}\) of size \(\lvert A\rvert=k\) there exist primes \(p_1,\ldots,p_r\) such that \(>r\) many \(a\in A\) are only divisible by primes from \(\{p_1,\ldots,p_r\}\).

Is it true that

\[2\pi(n^{1/2})-f(\pi(n)+1,n)\to \infty\]

as \(n\to \infty\)?

This is the first part. The primes may depend on \(A\). Erdős and Straus conjectured this [Er70b, p. 138 and p. 140].

The answer is no: Liam Price and GPT-5.5 Pro showed on the forum that \(f(\pi(n)+1,n)=2\pi(n^{1/2})+1\) for infinitely many \(n\); see the explanation by Nat Sothanaphan. Write \(p_k\) for the \(k\)-th prime. By [Po79, Corollary after Theorem 2.2] there are infinitely many \(N\) with \(p_{N-i}p_{N+i}\lt p_N^2\) for \(1\leq i\lt N\). Take \(n=p_N^2-1\), so \(\pi(n^{1/2})=N-1\). Let \(A\) consist of the products of adjacent primes on the path \(p_{2N-1},p_1,p_{2N-2},p_2,\ldots,p_{N+1},p_{N-1},p_N\), its two endpoint primes, and the other primes up to \(n\). Then \(\lvert A\rvert=\pi(n)+1\), and for any \(r\leq 2N-2\) primes at most \(r\) elements of \(A\) are divisible only by those primes, so \(f(\pi(n)+1,n)\geq 2N-1\).

theorem erdos_983.parts.i :
    ¬ Tendsto (fun n : ℕ ↦
      2 * (Nat.primeCounting (Nat.sqrt n) : ℤ) - (f (Nat.primeCounting n + 1) n : ℤ))
      atTop atTop

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

Erdos983.erdos_983.parts.ii

Open: stated without proof.

Let \(n\geq 2\) and \(\pi(n)\lt k\leq n\). Let \(f(k,n)\) be the smallest integer \(r\) such that in any \(A\subseteq \{1,\ldots,n\}\) of size \(\lvert A\rvert=k\) there exist primes \(p_1,\ldots,p_r\) such that \(>r\) many \(a\in A\) are only divisible by primes from \(\{p_1,\ldots,p_r\}\).

In general, estimate \(f(k,n)\), particularly when \(\pi(n)+1\lt k=o(n)\).

This is the second part. We read "estimate" as an asymptotic formula answer k n, valid for every function \(k=k(n)\) with \(\pi(n)+1\lt k(n)=o(n)\).

theorem erdos_983.parts.ii :
    ∀ k : ℕ → ℕ, (∀ᶠ n : ℕ in atTop, Nat.primeCounting n + 1 < k n) →
      ((fun n : ℕ ↦ (k n : ℝ)) =o[atTop] (fun n : ℕ ↦ (n : ℝ))) →
      (fun n : ℕ ↦ (f (k n) n : ℝ)) ~[atTop]
        (fun n : ℕ ↦ erdos_983.parts.ii.answer (k n) n)

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

Erdos983.erdos_983.variants.le_primeCounting

Textbook result, stated without proof.

It is trivial that \(f(k,n)\leq \pi(n)\) [Er70b, p. 138]. Here \(\pi(n)\lt k\).

theorem erdos_983.variants.le_primeCounting {k n : ℕ} (hk : Nat.primeCounting n < k) :
    f k n ≤ Nat.primeCounting n

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

Erdos983.erdos_983.variants.upper_bound

Solved: stated here without proof.

Erdős and Straus [Er70b, p. 139, (14)] proved

\[f(\pi(n)+1,n)\leq 2\pi(n^{1/2})+1.\]

theorem erdos_983.variants.upper_bound (n : ℕ) :
    f (Nat.primeCounting n + 1) n ≤ 2 * Nat.primeCounting (Nat.sqrt n) + 1

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

Erdos983.erdos_983.variants.erdos_straus

Solved: stated here without proof.

Erdős and Straus proved [Er70b, pp. 138-140] that

\[f(\pi(n)+1,n)=2\pi(n^{1/2})+o_A\left(\frac{n^{1/2}}{(\log n)^A}\right)\]

for any \(A>0\).

theorem erdos_983.variants.erdos_straus :
    ∀ A : ℝ, 0 < A →
      (fun n : ℕ ↦ (f (Nat.primeCounting n + 1) n : ℝ) -
          2 * (Nat.primeCounting (Nat.sqrt n) : ℝ)) =o[atTop]
        (fun n : ℕ ↦ Real.sqrt n / Real.log n ^ A)

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

Sources

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

LeanErdos983.erdos_983.parts.i · Erdos983.erdos_983.parts.ii · Erdos983.erdos_983.variants.le_primeCounting · Erdos983.erdos_983.variants.upper_bound · Erdos983.erdos_983.variants.erdos_straus

TheoremErdős Problem 985#

Reference: erdosproblems.com/985

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

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

Erdos985.erdos_985

Open: stated without proof.

Is it true that, for every prime \(p\), there is a prime \(q \leq p\) which is a primitive root modulo \(p\)?

theorem erdos_985 : ∀ᵉ (p : ℕ) (hp_prime : p.Prime) (hp_nontrivial : p ≠ 2),
    ∃ q, q.Prime ∧ q < p ∧ orderOf (q : ZMod p) = p - 1

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

Erdos985.erdos_985.variants.two_three_five_primitive_root

Solved: stated here without proof.

Heath-Brown proved that at least one of 2, 3, or 5 is a primitive root for infinitely many primes \(p\).

theorem erdos_985.variants.two_three_five_primitive_root :
    Set.Infinite
      {p : ℕ | p.Prime ∧
      (orderOf (2 : ZMod p) = p - 1 ∨
       orderOf (3 : ZMod p) = p - 1 ∨
       orderOf (5 : ZMod p) = p - 1)}

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

Sources

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

LeanErdos985.erdos_985 · Erdos985.erdos_985.variants.two_three_five_primitive_root

TheoremErdős Problem 986#

References: - erdosproblems.com/986 - [ChGr98] Chung, F. and Graham, R., Erdős on Graphs: His Legacy of Unsolved Problems. A K Peters, Ltd. (1998). - [Br26] Bradač, D., Off-diagonal Ramsey numbers. arXiv:2605.28793 (2026). - [Sp77] Spencer, J., Asymptotic lower bounds for Ramsey functions. Discrete Math. (1977), 69-76. - [MaVe23] Mattheus, S. and Verstraëte, J., The asymptotics of \(r(4,t)\). Ann. of Math. (2024), 941-965.

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

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

Erdos986.erdos_986

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

For any fixed \(s\geq 3\),

\[R(s,k) \gg \frac{k^{s-1}}{(\log k)^c}\]

for some constant \(c=c(s)>0\).

According to Chung and Graham [ChGr98] this was first conjectured by Erdős in 1947.

Proved by Bradač [Br26], with \(c=2s-4\).

The linked formal proof (Codex and GPT-5.6 Sol) gives k ^ (s - 1) / (log k) ^ c = O(R(s, k)) for a natural c > 0, with the Ramsey number defined through CliqueFree/IndepSetFree; this implies the statement below.

theorem erdos_986 :
    ∀ (s : ℕ) (hs : 3 ≤ s),
      ∃ (c C : ℝ), 0 < c ∧ 0 < C ∧
        ∀ᶠ (k : ℕ) in atTop,
          (SimpleGraph.classicalRamsey s k : ℝ) ≥
            C * (k : ℝ) ^ (s - 1) / (Real.log k) ^ c

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

Sources

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

LeanErdos986.erdos_986

TheoremErdős Problem 987#

References: - erdosproblems.com/987 - [APSSV26b] B. Alexeev, M. Putterman, M. Sawhney, M. Sellke, and G. Valiant, Short proofs in combinatorics, probability, and number theory II. arXiv:2604.06609 (2026). - [Cl67] Clunie, J., On a problem of Erdős. J. London Math. Soc. (1967), 133--136. - [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65. - [Er65b] Erdős, P., Some remarks on number theory. Israel J. Math. (the actual reference cited by Clunie 1967 as [2]; the erdosproblems.com bibliography points to a different Erdős 1965 paper, "Some recent advances and current problems in number theory" (Lectures on Modern Mathematics III, 1965, 196-244), which does not appear to contain the exponential-sum log-bound proof). - [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180. - [Li69] Lindström, B., An inequality for \(B_2\)-sequences. J. Combinatorial Theory (1969), 211-212.

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

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

Erdos987.erdos_987.parts.i

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Question 1:

Is it true that \(\limsup_{k \to \infty} A_k = \infty\)?

Erdős [Er64b] remarks it is "easy to see" that \(\limsup_k \sup_n |\sum_{j \le n} e(k x_j)| = \infty\). Erdős [Er65b] later found a "very easy" proof that \(A_k \gg \log k\) for infinitely many \(k\). Clunie [Cl67] proved that \(A_k \gg k^{1/2}\) for infinitely many \(k\), which implies the answer is yes (Tao independently found a proof). This is Problem 7.21 in [Ha74].

theorem erdos_987.parts.i :
    ∀ (x : ℕ → ℝ) (_ : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1),
      atTop.limsup (fun k : ℕ => A x k) = ⊤

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 74.

Erdos987.erdos_987.variants.sup_limsup_infty

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Erdős [Er64b] remarks it is "easy to see" that for every infinite sequence \(x_1, x_2, \ldots \in (0, 1)\),

\[\limsup_{k \to \infty} \sup_n \left\lvert \sum_{j \le n} e(k x_j) \right\rvert = \infty.\]

theorem erdos_987.variants.sup_limsup_infty
    (x : ℕ → ℝ) (hx : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1) :
    atTop.limsup (fun k : ℕ =>
      ⨆ n : ℕ, ((‖∑ j ∈ range n, e ((k : ℝ) * x j)‖ : ℝ) : EReal)) = ⊤

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 85.

Erdos987.erdos_987.variants.log_lower_bound

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Erdős [Er65b] proved that, for every infinite sequence \(x_1, x_2, \ldots \in (0, 1)\), \(A_k \gg \log k\) for infinitely many \(k\).

theorem erdos_987.variants.log_lower_bound
    (x : ℕ → ℝ) (_hx : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1) :
    ∃ c > 0, ∃ᶠ k : ℕ in atTop, ((c * Real.log k : ℝ) : EReal) ≤ A x k

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 96.

Erdos987.erdos_987.variants.sqrt_lower_bound

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Clunie [Cl67] proved that, for every infinite sequence \(x_1, x_2, \ldots \in (0, 1)\), \(A_k \gg k^{1/2}\) for infinitely many \(k\). (Tao independently found a proof.)

theorem erdos_987.variants.sqrt_lower_bound
    (x : ℕ → ℝ) (hx : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1) :
    ∃ c > 0, ∃ᶠ k : ℕ in atTop, ((c * Real.sqrt k : ℝ) : EReal) ≤ A x k

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 106.

Erdos987.erdos_987.variants.linear_upper_bound_weak

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Linear upper bound (weakened). A first weakened version of Clunie's A_k ≤ k: there exists a sequence \(x \in (0,1)\) with \(A_k \le 2k\) for all \(k \ge 1\). The witness is the (shifted) van der Corput sequence. For the tighter \(A_k \le k + 1\) bound see linear_upper_bound_clunie.

theorem erdos_987.variants.linear_upper_bound_weak :
    ∃ (x : ℕ → ℝ) (_ : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1),
      ∀ k : ℕ, 1 ≤ k → A x k ≤ ((2 * k : ℝ) : EReal)

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 118.

Erdos987.erdos_987.variants.linear_upper_bound_clunie

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Linear upper bound (tight via Clunie phase tracking). Tighter than linear_upper_bound_weak: there exists a sequence \(x \in (0,1)\) with \(A_k \le k + 1\) for all \(k \ge 1\), via the (shifted) van der Corput sequence. Whether the \(+1\) can be eliminated to recover Clunie's exact \(A_k \le k\) under the strict \(\mathrm{Ioo}\,0\,1\) hypothesis is open in this formalization (see linear_upper_bound).

theorem erdos_987.variants.linear_upper_bound_clunie :
    ∃ (x : ℕ → ℝ) (_ : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1),
      ∀ k : ℕ, 1 ≤ k → A x k ≤ (((k : ℝ) + 1) : EReal)

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 131.

Erdos987.erdos_987.variants.linear_upper_bound

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Clunie [Cl67] proved that there exists an infinite sequence \(\{z_\nu\}\) on the unit circle with \(A_\nu \le \nu\) for all \(\nu \ge 1\). Translating \(z_\nu = e(x_\nu)\), the natural domain of \(x_\nu\) is the half-open unit interval \(\mathrm{Ico}\,0\,1\), matching the original [Er64b]/[Cl67] statement (any unit complex number is allowed, including \(z = 1\), i.e. \(x = 0\)).

Note: erdosproblems.com/987 phrases the problem with the open interval \(x_\nu \in (0, 1)\), which excludes \(z = 1\) and is strictly stronger than what [Er64b]/[Cl67] state; we align with the original papers here. The shifted-vdc \(\le k + 1\) variant under the open interval is preserved as linear_upper_bound_clunie.

theorem erdos_987.variants.linear_upper_bound :
    ∃ (x : ℕ → ℝ) (_ : ∀ j : ℕ, x j ∈ Set.Ico (0 : ℝ) 1),
      ∀ k : ℕ, 1 ≤ k → A x k ≤ ((k : ℝ) : EReal)

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 148.

Erdos987.erdos_987.variants.sqrt_log_upper_bound

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

An internal OpenAI model (see [APSSV26b, §3]) proved that there exists an infinite sequence \(x_1, x_2, \ldots \in (0, 1)\) such that \(\sup_n \left\lvert \sum_{j \le n} e(k x_j) \right\rvert \ll (k \log k)^{1/2}\) for all \(k \ge 1\) (in particular \(A_k \ll (k \log k)^{1/2}\)).

Note: the bound is restricted to \(k \ge 2\) since \(\log 1 = 0\) would make the RHS vanish at \(k = 1\), while the LHS \(\|\sum_{j < n} e(x_j)\|\) can equal \(1\) (e.g. for \(n = 1\)).

theorem erdos_987.variants.sqrt_log_upper_bound :
    ∃ (x : ℕ → ℝ) (_ : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1) (C : ℝ) (_ : 0 < C),
      ∀ k n : ℕ, 2 ≤ k → ‖∑ j ∈ range n, e (k * x j)‖ ≤ C * Real.sqrt (k * Real.log k)

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 163.

Erdos987.erdos_987.parts.ii

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Question 2 (parts.ii): Is it possible for \(A_k = o(k)\)? Yes — there exists a sequence \((x_n) \in (0, 1)\) and a bound \(b(k) = o(k)\) with \(A x k \le b k\) eventually. A corollary of sqrt_log_upper_bound (which gives a \(\sqrt{k \log k}\) bound) plus the asymptotic \(\sqrt{k \log k} = o(k)\).

theorem erdos_987.parts.ii :
    ∃ (x : ℕ → ℝ) (_ : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1) (b : ℕ → ℝ),
      b =o[atTop] (fun k : ℕ => (k : ℝ)) ∧ ∀ᶠ k : ℕ in atTop, A x k ≤ ((b k : ℝ) : EReal)

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 177.

Erdos987.erdos_987.variants.finite_distinct_points

Solved: stated here; a Lean proof is at https://github.com/Marti2203/formal-conjectures/blob/19c63d48acce3099c242b059518c49bf8dc0eab8/FormalConjectures/ErdosProblems/987.lean.

Liu [Li69] showed that, for any \(\epsilon > 0\), \(A_k \gg k^{1 - \epsilon}\) infinitely often under the additional assumption that there are only a finite number of distinct points. Clunie observed in the Mathscinet review of [Li69] that under this assumption in fact \(A_k = \infty\) infinitely often (the version stated here).

theorem erdos_987.variants.finite_distinct_points
    (x : ℕ → ℝ) (_hx : ∀ j : ℕ, x j ∈ Set.Ioo (0 : ℝ) 1)
    (hfin : (Set.range x).Finite) :
    ∃ᶠ k : ℕ in atTop, A x k = ⊤

Category research solved; AMS 11 Number theory, 40 Sequences, series, summability, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/987.lean, line 189.

Sources

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

LeanErdos987.erdos_987.parts.i · Erdos987.erdos_987.variants.sup_limsup_infty · Erdos987.erdos_987.variants.log_lower_bound · Erdos987.erdos_987.variants.sqrt_lower_bound · Erdos987.erdos_987.variants.linear_upper_bound_weak · Erdos987.erdos_987.variants.linear_upper_bound_clunie · Erdos987.erdos_987.variants.linear_upper_bound · Erdos987.erdos_987.variants.sqrt_log_upper_bound · Erdos987.erdos_987.parts.ii · Erdos987.erdos_987.variants.finite_distinct_points

TheoremErdős Problem 990#

References: - erdosproblems.com/990 - [APSSV26b] B. Alexeev, M. Putterman, M. Sawhney, M. Sellke, and G. Valiant, Short proofs in combinatorics, probability, and number theory II. arXiv:2604.06609 (2026). - [ErTu50] Erdős, P. and Turán, P., On the distribution of roots of polynomials. Ann. of Math. (2) (1950), 105-119. - [Ha72b] Hayman, W. K., Angular value distribution of power series with gaps. Proc. London Math. Soc. (3) (1972), 590-624.

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

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

Erdos990.erdos_990

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

Let \(f=a_0+\cdots+a_dx^d\in \mathbb{C}[x]\) be a polynomial. Is it true that, if \(f\) has roots \(z_1,\ldots,z_d\) with corresponding arguments \(\theta_1,\ldots,\theta_d\in [0,2\pi]\), then for all intervals \(I\subseteq [0,2\pi]\)

\[ \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \ll \left(n\log M\right)^{1/2}, \]

where \(n\) is the number of non-zero coefficients of \(f\) and

\[ M=\frac{\lvert a_0\rvert+\cdots +\lvert a_d\rvert}{(\lvert a_0\rvert\lvert a_d\rvert)^{1/2}}. \]

An internal OpenAI model (see [APSSV26b]) has disproved the conjecture, constructing, for every \(n\geq 1\), a polynomial \(f\) with \(n\) non-zero coefficients such that \(M<3\) and with a positive real zero of multiplicity \(n-1\), whence letting \(I=[0,c/d]\) for a suitably small \(c>0\),

\[ \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \geq n-1. \]

theorem erdos_990 :
    ¬ ∃ C : ℝ, ∀ f : ℂ[X], f.coeff 0 ≠ 0 → ∀ α β : ℝ, 0 ≤ α → α ≤ β → β ≤ 2 * π →
      |(rootArgCount f (Set.Icc α β) : ℝ) - (β - α) / (2 * π) * (f.natDegree : ℝ)| ≤
        C * Real.sqrt ((f.support.card : ℝ) * Real.log (M f))

Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/990.lean, line 80.

Erdos990.erdos_990.variants.erdos_turan

Solved: stated here without proof.

Erdős and Turán [ErTu50] proved such an upper bound with \(n\) replaced by \(d\).

theorem erdos_990.variants.erdos_turan :
    ∃ C : ℝ, ∀ f : ℂ[X], f.coeff 0 ≠ 0 → ∀ α β : ℝ, 0 ≤ α → α ≤ β → β ≤ 2 * π →
      |(rootArgCount f (Set.Icc α β) : ℝ) - (β - α) / (2 * π) * (f.natDegree : ℝ)| ≤
        C * Real.sqrt ((f.natDegree : ℝ) * Real.log (M f))

Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/990.lean, line 90.

Erdos990.erdos_990.variants.hayman

Solved: stated here without proof.

Hayman [Ha72b] proved

\[ \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \leq n-1, \]

and noted this is essentially sharp since \(f(x)=(x^{p}-1)^{n-1}\) has \(n\) non-zero coefficients and has \(1\) as a positive real zero of multiplicity \(n-1\) (although for this \(f\) the parameter \(M\) becomes very large).

theorem erdos_990.variants.hayman :
    ∀ f : ℂ[X], f.coeff 0 ≠ 0 → ∀ α β : ℝ, 0 ≤ α → α ≤ β → β ≤ 2 * π →
      |(rootArgCount f (Set.Icc α β) : ℝ) - (β - α) / (2 * π) * (f.natDegree : ℝ)| ≤
        (f.support.card : ℝ) - 1

Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/990.lean, line 106.

Erdos990.erdos_990.variants.counterexample

Solved: stated here without proof.

An internal OpenAI model (see [APSSV26b]) has disproved the conjecture, constructing, for every \(n\geq 1\), a polynomial \(f\) with \(n\) non-zero coefficients such that \(M<3\) and with a positive real zero of multiplicity \(n-1\).

theorem erdos_990.variants.counterexample :
    ∀ n : ℕ, 1 ≤ n → ∃ f : ℂ[X], f.coeff 0 ≠ 0 ∧ f.support.card = n ∧ M f < 3 ∧
      ∃ x : ℝ, 0 < x ∧ f.rootMultiplicity (x : ℂ) = n - 1

Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/990.lean, line 118.

Sources

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

LeanErdos990.erdos_990 · Erdos990.erdos_990.variants.erdos_turan · Erdos990.erdos_990.variants.hayman · Erdos990.erdos_990.variants.counterexample

TheoremErdős Problem 994#

References: - erdosproblems.com/994 - [Er64b] Erdős, P., Problems and results on diophantine approximations. Compositio Math. (1964), 52-65. - [Kh23] Khintchine, A., Ein Satz über Kettenbrüche, mit arithmetischen Anwendungen. Math. Z. (1923), 289--306. - [Ma70] Marstrand, J. M., On Khinchin's conjecture about strong uniform distribution. Proc. London Math. Soc. (3) (1970), 540--556.

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

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

Erdos994.erdos_994

Solved: stated here without proof.

Let \(E\subseteq (0,1)\) be a meaurable subset with Lebesgue measure \(\lambda(E)\). Is it true that, for almost all \(\alpha\),

\[\lim_{n\to \infty}\frac{1}{n}\sum_{1\leq k\leq n}1_{\{k\alpha \}\in E}=\lambda(E)\]

for all \(E\)?

This is a conjecture of Khintchine [Kh23] (with the exceptional null set of \(\alpha\) allowed to depend on \(E\)). It is false, and was disproved by Marstrand [Ma70].

theorem erdos_994 :
    ¬ ∀ E ⊆ Ioo (0 : ℝ) 1, MeasurableSet E →
      ∀ᵐ α : ℝ, Tendsto (visitAverage E α) atTop (nhds (volume E).toReal)

Category research solved; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/994.lean, line 55.

Erdos994.erdos_994.variants.simultaneous

Textbook result, proved here.

Read literally, with "for almost all \(\alpha\)" placed before "for all \(E\)", the statement is trivially false: for any \(\alpha\), removing the countable orbit \(\{\{k\alpha\} : k\geq 1\}\) from \((0,1)\) gives a measurable set of measure \(1\) which is never visited.

theorem erdos_994.variants.simultaneous :
    ¬ ∀ᵐ α : ℝ, ∀ E ⊆ Ioo (0 : ℝ) 1, MeasurableSet E →
      Tendsto (visitAverage E α) atTop (nhds (volume E).toReal)

Category textbook; AMS 11 Number theory, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/994.lean, line 66.

Sources

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

LeanErdos994.erdos_994 · Erdos994.erdos_994.variants.simultaneous

TheoremErdős Problem 995#

References: - erdosproblems.com/995 - [Er49] Erdős, P., On the strong law of large numbers, Trans. Amer. Math. Soc. (1949), 329-334.

Let \(n_1 < n_2 < \cdots\) be a lacunary sequence of integers and \(f \in L^2([0,1])\) with \(\int_0^1 f = 0\). Estimate the growth of

\[S_N(\alpha) = \sum_{k \le N} f(\{\alpha n_k\})\]

for almost all \(\alpha\), where \(\{\cdot\}\) denotes the fractional part. In particular, is it true that \(S_N(\alpha) = o\!\left(N \sqrt{\log\log N}\right)\) for almost all \(\alpha\)?

Erdős [Er49] constructed a lacunary sequence and a mean-zero \(f \in L^2([0,1])\) for which, for every \(\varepsilon > 0\), \(\limsup_N S_N(\alpha) / (N (\log\log N)^{1/2 - \varepsilon}) = \infty\) for almost all \(\alpha\), and believed this lower bound to be close to the truth.

The mean-zero hypothesis \(\int_0^1 f = 0\) is the natural normalisation: otherwise the sum has a linear main term coming from the average of \(f\).

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

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

Erdos995.erdos_995

Open: stated without proof.

Erdős Problem 995:

For every lacunary sequence \((n_k)\) of integers and every \(f \in L^2([0,1])\) with \(\int_0^1 f = 0\), is it true that for almost all \(\alpha\),

\[\sum_{k < N} f(\{\alpha n_k\}) = o\!\left(N \sqrt{\log\log N}\right)?\]

theorem erdos_995 :
    ∀ (n : ℕ → ℕ), IsLacunary n → ∀ (f : ℝ → ℝ),
      MemLp f 2 (volume.restrict (Icc (0 : ℝ) 1)) →
      ∫ x in (0 : ℝ)..1, f x = 0 →
      ∀ᵐ α ∂(volume.restrict (Icc (0 : ℝ) 1)),
        partialSum n f α =o[atTop] fun N => (N : ℝ) * Real.sqrt (Real.log (Real.log N))

Category research open; AMS 11 Number theory, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/995.lean, line 60.

Erdos995.erdos_995.variants.erdos_lower_bound

Solved: stated here without proof.

Erdős [Er49] showed the growth cannot be pushed below \(N (\log\log N)^{1/2}\) by more than an arbitrarily small power: there is a lacunary sequence and a mean-zero \(f \in L^2([0,1])\) such that for every \(\varepsilon > 0\), for almost all \(\alpha\),

\[\limsup_{N \to \infty} \frac{\sum_{k < N} f(\{\alpha n_k\})}{N (\log\log N)^{1/2 - \varepsilon}} = \infty.\]

theorem erdos_995.variants.erdos_lower_bound :
    ∃ (n : ℕ → ℕ), IsLacunary n ∧ ∃ (f : ℝ → ℝ),
      MemLp f 2 (volume.restrict (Icc (0 : ℝ) 1)) ∧
      ∫ x in (0 : ℝ)..1, f x = 0 ∧
      ∀ ε > (0 : ℝ),
        ∀ᵐ α ∂(volume.restrict (Icc (0 : ℝ) 1)),
          atTop.limsup (fun N => (((partialSum n f α N) /
            ((N : ℝ) * (Real.log (Real.log N)) ^ ((1 : ℝ) / 2 - ε)) : ℝ) : EReal)) = ⊤

Category research solved; AMS 11 Number theory, 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/995.lean, line 76.

Sources

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

LeanErdos995.erdos_995 · Erdos995.erdos_995.variants.erdos_lower_bound

TheoremErdős Problem 996#

Reference: - erdosproblems.com/996 - [Er49d] Erdös, P. "On the strong law of large numbers." Transactions of the American Mathematical Society 67.1 (1949): 51-56. - [Ma66] Matsuyama, Noboru. "On the strong law of large numbers." Tohoku Mathematical Journal, Second Series 18.3 (1966): 259-269.

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

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

Erdos996.erdos_996

Open: stated without proof.

Does there exists a positive constant C such that for all f ∈ L²[0,1] and all lacunary sequences n, if ‖f - fₖ‖₂ = O(1 / log log log k ^ C), then for almost every x, lim ∑ k ∈ Finset.range N, f (n k • x)) / N = ∫ t, f t ∂t?

theorem erdos_996 :
    ∃ (C : ℝ), 0 < C ∧ ∀ (f : Lp ℂ 2 (haarAddCircle (T := 1))) (n : ℕ → ℕ),
    IsLacunary n →
    (fun k => (eLpNorm (⇑f - fourierPartial f k) 2 (haarAddCircle (T := 1))).toReal) =O[atTop]
    (fun k => 1 / (log (log (log k))) ^ C)
    →
    ∀ᵐ x, Tendsto (fun N => (∑ k ∈ .range N, f (n k • x)) / N) atTop
    (𝓝 (∫ t, f t ∂haarAddCircle))

Category research open; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/996.lean, line 45.

Erdos996.erdos_996.variants.log2

Solved: stated here without proof.

The following theorem is proved in [Ma66].

theorem erdos_996.variants.log2 : ∀ (C : ℝ), 0.5 < C →
    ∀ (f : Lp ℂ 2 (haarAddCircle (T := 1))) (n : ℕ → ℕ),
    IsLacunary n →
    (fun k => (eLpNorm (⇑f - fourierPartial f k) 2 (haarAddCircle (T := 1))).toReal) =O[atTop]
    (fun k => 1 / (log (log k)) ^ C)
    →
    ∀ᵐ x, Tendsto (fun N => (∑ k ∈ .range N, f (n k • x)) / N) atTop
    (𝓝 (∫ t, f t ∂haarAddCircle))

Category research solved; AMS 42 Harmonic analysis on Euclidean spaces. Declared in FormalConjectures/ErdosProblems/996.lean, line 57.

Sources

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

LeanErdos996.erdos_996 · Erdos996.erdos_996.variants.log2

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.