Erdős Problem 500 to Erdős Problem 525

TheoremErdős Problem 500#

References: - erdosproblems.com/500 - [Ra10] Razborov, Alexander A., On 3-hypergraphs with forbidden 4-vertex configurations. SIAM J. Discrete Math. (2010), 946-963. - [BaTa11] Baber, Rahil and Talbot, John, Hypergraphs do jump. Combin. Probab. Comput. (2011), 161-171. - [Ba12] Baber, Rahil, Turán densities of hypercubes. arXiv:1201.3587 (2012). - [JPILY26] Jeong, Gyeongwon and Park, Seonghun and Im, Seonghyuk and Lee, Joonkyung and Yang, Hongseok, A New Upper Bound for the Turán Density of the Tetrahedron. arXiv:2609.27495 (2026).

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

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

Erdos500.erdos_500

Open: stated without proof.

What is \(\mathrm{ex}_3(n,K_4^3)\)? That is, the largest number of \(3\)-edges which can placed on \(n\) vertices so that there exists no \(K_4^3\), a set of 4 vertices which is covered by all 4 possible \(3\)-edges.

See also 712 for the general case.

theorem erdos_500 :
    (fun n ↦ Hypergraph.cliqueExtremalNumber n 3 4) = erdos_500.answer

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

Erdos500.erdos_500.variants.lower_bound

Solved: stated here without proof.

A problem of Turán. Turán observed that dividing the vertices into three equal parts \(X_1,X_2,X_3\), and taking the edges to be those triples that either have exactly one vertex in each part or two vertices in \(X_i\) and one vertex in \(X_{i+1}\) (where \(X_4=X_1\)) shows that

\[\mathrm{ex}_3(n,K_4^3)\geq\left(\frac{5}{9}+o(1)\right)\binom{n}{3}.\]

theorem erdos_500.variants.lower_bound (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop,
      (5 / 9 - ε) * (n.choose 3 : ℝ) ≤ Hypergraph.cliqueExtremalNumber n 3 4

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

Erdos500.erdos_500.variants.turan_conjecture

Open: stated without proof.

Turán observed that dividing the vertices into three equal parts \(X_1,X_2,X_3\), and taking the edges to be those triples that either have exactly one vertex in each part or two vertices in \(X_i\) and one vertex in \(X_{i+1}\) (where \(X_4=X_1\)) shows that

\[\mathrm{ex}_3(n,K_4^3)\geq\left(\frac{5}{9}+o(1)\right)\binom{n}{3}.\]

This is probably the truth.

theorem erdos_500.variants.turan_conjecture :
    (fun n ↦ (Hypergraph.cliqueExtremalNumber n 3 4 : ℝ)) ~[atTop]
      fun n ↦ 5 / 9 * (n.choose 3 : ℝ)

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

Erdos500.erdos_500.variants.upper_bound

Solved: stated here; a Lean proof is at https://github.com/taeyool/tetrahedron-turan/blob/28b83b6f215cb886d2abdc89b33fdae3f17a7e3f/LeanFlagAlgebras/Core/Examples/FullSevenConverged/TetrahedronDifferential.lean#L251.

The historical upper bound

\[\mathrm{ex}_3(n,K_4^3)\leq (0.561666+o(1))\binom{n}{3}\]

is due to Razborov [Ra10]. (erdosproblems.com gives \(0.5611666\) and omits the \(o(1)\); without it the bound fails at \(n=4\), where \(\mathrm{ex}_3(4,K_4^3)=3>0.561666\binom{4}{3}\).)

[Ra10, (2)] gives this bound in complementary form, as a result that numerical computations suggest, not as a theorem. [BaTa11] reproduce the computation.

Baber [Ba12, §5.1, p. 14] gives \(\pi(K_4^3)\leq 0.5615\), where \(\pi(K_4^3)\) is the Turán density of erdos_500.variants.asymptotic. Jeong, Park, Im, Lee and Yang [JPILY26, Theorem 1.1] prove that \(\pi(K_4^3)<0.557789\), with a formal proof in Lean 4. The bound above follows from either result.

theorem erdos_500.variants.upper_bound (ε : ℝ) (hε : 0 < ε) :
    ∀ᶠ n : ℕ in atTop,
      (Hypergraph.cliqueExtremalNumber n 3 4 : ℝ) ≤ (0.561666 + ε) * (n.choose 3 : ℝ)

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

Erdos500.erdos_500.variants.asymptotic

Open: stated without proof.

The asymptotic form of the question: what is the Turán density

\[\pi(K_4^3)=\lim_{n\to\infty}\frac{\mathrm{ex}_3(n,K_4^3)}{\binom{n}{3}}?\]

By erdos_500.variants.lower_bound, \(\pi(K_4^3)\geq\frac{5}{9}\). Turán's conjecture says that \(\pi(K_4^3)=\frac{5}{9}\).

theorem erdos_500.variants.asymptotic :
    Tendsto (fun n : ℕ ↦ (Hypergraph.cliqueExtremalNumber n 3 4 : ℝ) / (n.choose 3 : ℝ))
      atTop (𝓝 erdos_500.variants.asymptotic.answer)

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

Sources

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

LeanErdos500.erdos_500 · Erdos500.erdos_500.variants.lower_bound · Erdos500.erdos_500.variants.turan_conjecture · Erdos500.erdos_500.variants.upper_bound · Erdos500.erdos_500.variants.asymptotic

TheoremErdős Problem 501#

References: - erdosproblems.com/501 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. 6 (1961), 221-254. - [ErHa71] Erdős, Paul and Hajnal, András, Unsolved problems in set theory. Axiomatic Set Theory, Proc. Sympos. Pure Math. XIII Part I (1971), 17-48. - [ErHa60] Erdős, Paul and Hajnal, András. On some combinatorial problems involving complete graphs. Acta Math. Acad. Sci. Hungar. (1960), 395-424. - [Gl62] Gladysz, S. Some topological properties of independent sets. Colloq. Math. (1962). - [He72] Hechler, S. H. A dozen small uncountable cardinals. TOPO 72, Lecture Notes in Math. (1972), 207-218. - [NPS87] Newelski, L., Pawlikowski, J., and Seredyński, F. Infinite independent sets in the closed case. Acta Math. Acad. Sci. Hungar. (1987).

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

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

Erdos501.erdos_501

Open: stated without proof.

For every \(x \in \mathbb{R}\) let \(A_x \subset \mathbb{R}\) be a bounded set with outer measure \(< 1\). Must there exist an infinite independent set, that is, some infinite \(X \subseteq \mathbb{R}\) such that \(x \notin A_y\) for all \(x \neq y \in X\)?

If the sets \(A_x\) are closed and have measure \(< 1\), then must there exist an independent set of size \(3\)?

Known results: Erdős–Hajnal [ErHa60] proved the existence of arbitrarily large finite independent sets. Hechler [He72] showed the answer is no assuming the continuum hypothesis.

theorem erdos_501 :
    ∀ (A : ℝ → Set ℝ),
      (∀ x, Bornology.IsBounded (A x)) →
      (∀ x, volume.toOuterMeasure (A x) < 1) →
      ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y)

Category research open; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 71.

Erdos501.erdos_501.variants.erdosHajnal_finite

Solved: stated here without proof.

Erdős–Hajnal (1960): arbitrarily large finite independent sets exist.

For every n : ℕ and every family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1, there exists a finite independent set of size at least n.

This was proved by Erdős and Hajnal [ErHa60].

theorem erdos_501.variants.erdosHajnal_finite :
    ∀ (n : ℕ) (A : ℝ → Set ℝ),
      (∀ x, Bornology.IsBounded (A x)) →
      (∀ x, volume.toOuterMeasure (A x) < 1) →
      ∃ X : Finset ℝ, n ≤ X.card ∧ (X : Set ℝ).Pairwise (fun x y => x ∉ A y)

Category research solved; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 88.

Erdos501.erdos_501.variants.hechler_CH

Solved: stated here without proof.

Hechler (1972) [He72]: the answer to the main question is NO, assuming the continuum hypothesis.

Assuming CH (ℵ₁ = 𝔠), there exists a family A : ℝ → Set ℝ of bounded sets with Lebesgue outer measure < 1 for which no infinite independent set exists.

theorem erdos_501.variants.hechler_CH :
    (ℵ₁ = 𝔠) →
    ∃ (A : ℝ → Set ℝ),
      (∀ x, Bornology.IsBounded (A x)) ∧
      (∀ x, volume.toOuterMeasure (A x) < 1) ∧
      ¬ ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y)

Category research solved; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 102.

Erdos501.erdos_501.variants.closed_size3

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

Closed sets case: existence of an independent set of size 3.

If the sets A x are closed with Lebesgue measure < 1, must there exist an independent set of size 3?

This is implied by the stronger theorem of Newelski–Pawlikowski–Seredyński [NPS87] below; Gladysz [Gl62] earlier proved the existence of an independent set of size 2.

theorem erdos_501.variants.closed_size3 :
    ∀ (A : ℝ → Set ℝ),
      (∀ x, IsClosed (A x)) →
      (∀ x, volume (A x) < 1) →
      ∃ X : Set ℝ, 3 ≤ X.ncard ∧ X.Pairwise (fun x y => x ∉ A y)

Category research solved; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 121.

Erdos501.erdos_501.variants.newelski_pawlikowski_seredynski

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

Newelski–Pawlikowski–Seredyński (1987) [NPS87]: infinite independent set in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there is an infinite independent set. This gives a strong affirmative answer to the second question of Problem 501.

theorem erdos_501.variants.newelski_pawlikowski_seredynski :
    ∀ (A : ℝ → Set ℝ),
      (∀ x, IsClosed (A x)) →
      (∀ x, volume (A x) < 1) →
      ∃ X : Set ℝ, X.Infinite ∧ X.Pairwise (fun x y => x ∉ A y)

Category research solved; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 137.

Erdos501.erdos_501.variants.gladysz_size2

Solved: stated here without proof.

Gladysz (1962) [Gl62]: independent set of size 2 in the closed case.

If all the sets A x are closed with Lebesgue measure < 1, then there exist two distinct reals x y such that x ∉ A y and y ∉ A x.

This is a weaker result proved by Gladysz before the full Newelski–Pawlikowski– Seredyński theorem [NPS87].

theorem erdos_501.variants.gladysz_size2 :
    ∀ (A : ℝ → Set ℝ),
      (∀ x, IsClosed (A x)) →
      (∀ x, volume (A x) < 1) →
      ∃ X : Set ℝ, 2 ≤ X.ncard ∧ X.Pairwise (fun x y => x ∉ A y)

Category research solved; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 153.

Erdos501.erdos_501.variants.singleton_independent

Textbook result, proved here.

Trivial lower bound: a single-element set is always independent.

For any family A, any singleton {x} is vacuously independent: there are no two distinct elements.

theorem erdos_501.variants.singleton_independent (A : ℝ → Set ℝ) (x : ℝ) :
    ({x} : Set ℝ).Pairwise (fun x y => x ∉ A y)

Category textbook; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 166.

Erdos501.erdos_501.variants.pair_independent_iff

Textbook result, proved here.

Two-element sets: independent iff mutual non-membership.

A two-element set {x, y} (with x ≠ y) is independent for A if and only if x ∉ A y and y ∉ A x.

theorem erdos_501.variants.pair_independent_iff (A : ℝ → Set ℝ) {x y : ℝ} (hxy : x ≠ y) :
    ({x, y} : Set ℝ).Pairwise (fun x y => x ∉ A y) ↔ x ∉ A y ∧ y ∉ A x

Category textbook; AMS 05 Combinatorics, 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/501.lean, line 176.

Sources

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

LeanErdos501.erdos_501 · Erdos501.erdos_501.variants.erdosHajnal_finite · Erdos501.erdos_501.variants.hechler_CH · Erdos501.erdos_501.variants.closed_size3 · Erdos501.erdos_501.variants.newelski_pawlikowski_seredynski · Erdos501.erdos_501.variants.gladysz_size2 · Erdos501.erdos_501.variants.singleton_independent · Erdos501.erdos_501.variants.pair_independent_iff

TheoremErdős Problem 502#

References: - erdosproblems.com/502 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [BBS83] Bannai, Eiichi and Bannai, Etsuko and Stanton, Dennis, An upper bound for the cardinality of an \(s\)-distance subset in real Euclidean space. II. Combinatorica (1983), 147-152. - [PePo21] Petrov, Fedor and Pohoata, Cosmin, A remark on sets with few distances in \(\mathbb{R}^d\). Proc. Amer. Math. Soc. (2021), 569-571.

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

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

Erdos502.erdos_502

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

What is the size of the largest \(A\subseteq \mathbb{R}^n\) such that there are only two distinct distances between elements of \(A\)? That is,

\[\# \{ \lvert x-y\rvert : x\neq y\in A\} = 2.\]

Asked to Erdős by Coxeter. Bannai, Bannai, and Stanton [BBS83] have proved that

\[\lvert A\rvert \leq \binom{n+2}{2}.\]

A simple proof of this upper bound was given by Petrov and Pohoata [PePo21].

The exact maximum is not known in general: a lower bound of \(\binom{n+1}{2}\) follows from the construction of Alweiss (see [503]).

theorem erdos_502 (n : ℕ) (A : Set (ℝ^n)) (hA : A.Finite)
    (hA2 : {d : ℝ | ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ dist x y = d}.ncard = 2) :
    A.ncard ≤ (n + 2).choose 2

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/502.lean, line 53.

Sources

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

LeanErdos502.erdos_502

TheoremErdős Problem 503#

Reference: erdosproblems.com/503

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

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

Erdos503.erdos_503

Open: stated without proof.

What is the size of the largest \(A \subseteq \mathbb{R}^n\) such that every three points from \(A\) determine an isosceles triangle? That is, for any three points \(x\), \(y\), \(z\) from \(A\), at least two of the distances \(|x - y|\), \(|y - z|\), \(|x - z|\) are equal.

theorem erdos_503 (n : ℕ) :
    IsGreatest {(A.ncard) | (A : Set (ℝ^n)) (hA : A.IsIsosceles)} erdos_503.answer

Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/503.lean, line 40.

Erdos503.erdos_503.variants.R2

Solved: stated here without proof.

When \(n = 2\), the answer is 6 (due to Kelly [ErKe47] - an alternative proof is given by Kovács [Ko24c]).

[ErKe47] Erdős, Paul and Kelly, L. M., Elementary Problems and Solutions: Solutions: E735. Amer. Math. Monthly (1947), 227-229. [Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024).

theorem erdos_503.variants.R2 :
    IsGreatest {(A.ncard) | (A : Set ℝ²) (hA : A.IsIsosceles)} 6

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/503.lean, line 51.

Erdos503.erdos_503.variants.R3

Solved: stated here without proof.

When \(n = 3\), the answer is 8 (due to Croft [Cr62]).

[Cr62] Croft, H. T., \(9\)-point and \(7\)-point configurations in \(3\)-space. Proc. London Math. Soc. (3) (1962), 400-424.

theorem erdos_503.variants.R3 :
    IsGreatest {(A.ncard) | (A : Set ℝ³) (hA : A.IsIsosceles)} 8

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/503.lean, line 61.

Erdos503.erdos_503.variants.upper_bound

Solved: stated here without proof.

The best upper bound known in general is due to Blokhius [Bl84] who showed that

\[ |A| \leq \binom{n + 2}{2} \]

[Bl84] Blokhuis, A., Few-distance sets. (1984), iv+70.

theorem erdos_503.variants.upper_bound (n : ℕ) :
    ∀ m ∈ {(A.ncard) | (A : Set (ℝ^n)) (hA : A.IsIsosceles)}, m ≤ (n + 2).choose 2

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/503.lean, line 74.

Erdos503.erdos_503.variants.lower_bound

Solved: stated here without proof.

Alweiss has observed a lower bound of \(\binom{n + 1}{2}\) follows from considering the subset of \(\mathbb{R}^{n + 1}\) formed of all vectors \(e_i + e_j\) where \(e_i\), \(e_j\) are distinct coordinate vectors. This set can be viewed as a subset of some \(\mathbb{R}^n\), and is easily checked to have the required property.

The bound is stated as the existence of such a set and not as a bound on the sSup of the sizes: in ℕ the sSup of an unbounded set is 0, so the latter would also assert that the sizes are bounded, which is the content of erdos_503.variants.upper_bound.

theorem erdos_503.variants.lower_bound (n : ℕ) :
    ∃ m ∈ {(A.ncard) | (A : Set (ℝ^n)) (hA : A.IsIsosceles)}, (n + 1).choose 2 ≤ m

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/503.lean, line 89.

Sources

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

LeanErdos503.erdos_503 · Erdos503.erdos_503.variants.R2 · Erdos503.erdos_503.variants.R3 · Erdos503.erdos_503.variants.upper_bound · Erdos503.erdos_503.variants.lower_bound

TheoremErdős Problem 504#

Reference: erdosproblems.com/504

Blumenthal's minimax angle problem: let \(\alpha_N\) be the supremum of all \(0 \le \alpha \le \pi\) such that every set of \(N\) points in the plane contains three distinct points determining an angle at least \(\alpha\). Determine \(\alpha_N\).

Szekeres [Sz41] proved \(\alpha_{2^n} \le \pi(1 - 1/n)\) together with a lower bound for \(2^n + 1\) points. Erdős and Szekeres [ErSz60] proved \(\alpha_{2^n} = \alpha_{2^n - 1} = \pi(1 - 1/n)\), and Sendov [Se95] determined \(\alpha_N\) for every \(N\).

[Sz41] Szekeres, G., On an extremum problem in the plane. Amer. J. Math. 63 (1941), 208-210.

[ErSz60] Erdős, P. and Szekeres, G., On some extremum problems in elementary geometry. Ann. Univ. Sci. Budapest. Eötvös Sect. Math. 3-4 (1960-61), 53-62.

[Se95] Sendov, Bl., Minimax of the angles in a plane configuration of points. Acta Math. Hungar. 69 (1995), 27-46. (Reviewed in Zbl 0853.52009, which states the main theorem as \(\alpha_N = \pi\left(1 - \frac{2}{2n+1}\right)\) for \(2^n < N \le 2^n + 2^{n-2}\) and \(\alpha_N = \pi\left(1 - \frac{1}{n+1}\right)\) for \(2^n + 2^{n-2} < N \le 2^{n+1}\), \(n \ge 2\).)

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

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

Erdos504.erdos_504

Solved: stated here without proof.

Erdős–Szekeres (1960). For \(n \ge 3\), \(\alpha_{2^n} = \pi\left(1 - \frac{1}{n}\right)\).

theorem erdos_504 {n : ℕ} (hn : 3 ≤ n) :
    minimaxAngle (2 ^ n) = (1 - 1 / (n : ℝ)) * π

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

Erdos504.erdos_504.variants.endpoint

Solved: stated here without proof.

Erdős–Szekeres (1960). For \(n \ge 3\), also \(\alpha_{2^n - 1} = \pi\left(1 - \frac{1}{n}\right)\).

theorem erdos_504.variants.endpoint {n : ℕ} (hn : 3 ≤ n) :
    minimaxAngle (2 ^ n - 1) = (1 - 1 / (n : ℝ)) * π

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

Erdos504.erdos_504.variants.erdos_szekeres_1960

Solved: stated here; a Lean proof is at https://github.com/ToshiDad/erdos-504/blob/fd344a9/Erdos504.lean#L6501.

The lower-bound half of erdos_504 in existential form (Theorem 1 of [ErSz60]): any \(2^n\) points of the plane contain three points determining an angle strictly greater than \(\pi(1 - 1/n)\).

theorem erdos_504.variants.erdos_szekeres_1960 {n : ℕ} (hn : 3 ≤ n)
    (S : Finset ℂ) (hcard : S.card = 2 ^ n) :
    ∃ p ∈ S, ∃ q ∈ S, ∃ r ∈ S, p ≠ q ∧ r ≠ q ∧
      (1 - 1 / (n : ℝ)) * π < EuclideanGeometry.angle p q r

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

Erdos504.erdos_504.variants.szekeres_lower

Solved: stated here; a Lean proof is at https://github.com/ToshiDad/erdos-504/blob/fd344a9/Erdos504.lean#L341.

Szekeres (1941), lower bound. More than \(2^n\) points of the plane contain three points determining an angle strictly greater than \(\pi(1 - 1/n)\).

theorem erdos_504.variants.szekeres_lower {n : ℕ} (hn : 0 < n) (S : Finset ℂ)
    (hcard : 2 ^ n < S.card) :
    ∃ p ∈ S, ∃ q ∈ S, ∃ r ∈ S, p ≠ q ∧ r ≠ q ∧
      (1 - 1 / (n : ℝ)) * π < EuclideanGeometry.angle p q r

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

Erdos504.erdos_504.variants.szekeres_upper

Solved: stated here; a Lean proof is at https://github.com/ToshiDad/erdos-504/blob/fd344a9/Erdos504.lean#L801.

Szekeres (1941), upper-bound construction. For every \(\varepsilon > 0\) there is a set of exactly \(2^t\) points of the plane all of whose angles are less than \(\pi(1 - 1/t) + \varepsilon\). Together with erdos_504.variants.erdos_szekeres_1960 this pins down \(\alpha_{2^t} = \pi(1 - 1/t)\) for \(t \ge 3\), where the supremum is approached but not attained by any finite configuration. (For \(t = 2\) it is attained: a square has all angles at most \(\pi/2 = \alpha_4\).)

theorem erdos_504.variants.szekeres_upper {t : ℕ} (ht : 0 < t) {ε : ℝ}
    (hε : 0 < ε) :
    ∃ S : Finset ℂ, S.card = 2 ^ t ∧
      ∀ p ∈ S, ∀ q ∈ S, ∀ r ∈ S, p ≠ q → r ≠ q →
        EuclideanGeometry.angle p q r < (1 - 1 / (t : ℝ)) * π + ε

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

Erdos504.erdos_504.variants.sendov

Solved: stated here without proof.

Sendov (1995). The complete determination: for \(n \ge 3\), \(\alpha_N = \pi(1 - 1/n)\) whenever \(2^{n-1} + 2^{n-3} < N \le 2^n\), and \(\alpha_N = \pi\left(1 - \frac{2}{2n - 1}\right)\) whenever \(2^{n-1} < N \le 2^{n-1} + 2^{n-3}\).

This is the statement of [Se95] (as given in Zbl 0853.52009) with \(n\) shifted by one. For \(n = 3\) the second branch gives \(\alpha_5 = 3\pi/5\), the value computed in [ErSz60], and \(\alpha_N\) is nondecreasing in \(N\) across the two branches. The problem page erdosproblems.com/504 prints the second branch as \(\pi(1 - \frac{1}{2n-1})\), which would give \(\alpha_5 = 4\pi/5 > \alpha_6\); that appears to be a typo.

theorem erdos_504.variants.sendov {n N : ℕ} (hn : 3 ≤ n)
    (h1 : 2 ^ (n - 1) < N) (h2 : N ≤ 2 ^ n) :
    minimaxAngle N =
      if 2 ^ (n - 1) + 2 ^ (n - 3) < N then (1 - 1 / (n : ℝ)) * π
      else (1 - 2 / (2 * (n : ℝ) - 1)) * π

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

Sources

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

LeanErdos504.erdos_504 · Erdos504.erdos_504.variants.endpoint · Erdos504.erdos_504.variants.erdos_szekeres_1960 · Erdos504.erdos_504.variants.szekeres_lower · Erdos504.erdos_504.variants.szekeres_upper · Erdos504.erdos_504.variants.sendov

TheoremErdős Problem 505#

Reference: erdosproblems.com/505

Borsuk's conjecture (1933): Is every bounded set of diameter 1 in \(\mathbb{R}^n\) the union of at most \(n + 1\) sets of diameter strictly less than 1?

Erdős [Er44] suspected this is false for sufficiently large \(n\). Confirmed by Kahn–Kalai [KK93], who disproved the conjecture for \(n \geq 2015\). Grinsztajn (2026) gave a counterexample for \(n = 63\); the smallest refereed counterexample was \(n = 64\) (Jenrich–Brouwer, 2014). In September 2026 an internal OpenAI model gave a counterexample for \(n = 9\) [OAI26], with a formal Lean proof; see Borsuk.borsuk_conjecture.not_nine.

The conjecture is true for \(n \leq 3\) (Eggleston [Eg55] for \(n = 3\)).

References

• [Bo33] Borsuk, K. (1933). Drei Sätze über die n-dimensionale euklidische Sphäre. Fund. Math. 20, 177–190.
• [Er44] Erdős, P. (1944). Remarks on a conjecture of Borsuk.
• [Eg55] Eggleston, H. G. (1955). Covering a three-dimensional set with sets of smaller diameter. J. London Math. Soc. 30, 11–24.
• [KK93] Kahn, J., Kalai, G. (1993). A counterexample to Borsuk's conjecture. Bull. Amer. Math. Soc. 29, 60–62.
• [OAI26] OpenAI (2026). A nine-dimensional counterexample to Borsuk's covering assertion. OpenAI Math Release preprint. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-nine-dimensional-counterexample-to-Borsuks-covering-assertion-September-23-2026/paper.pdf

This file points to the canonical formalization in FormalConjectures.Wikipedia.BorsukConjecture.

AI disclosure

Lean 4 code in this file was drafted with assistance from Claude (Anthropic). The mathematical content and references are the author's own work.

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

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

Erdos505.erdos_505

Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/96cd54930d844e3655e6bb89b96b65516397dae9/src/v4.24.0/ErdosProblems/Erdos505.lean#L1153.

Erdős Problem 505 (disproved). Borsuk's conjecture is false for sufficiently large \(n\): there exists a dimension \(n\) and a bounded set \(S \subseteq \mathbb{R}^n\) with at least two points that cannot be covered by \(n + 1\) subsets each of strictly smaller diameter.

Erdős [Er44] suspected this. Disproved by Kahn–Kalai [KK93] for \(n \geq 2015\). Currently known to be false for \(n = 9\) [OAI26] and for \(n \geq 63\). A formal proof was formalised by Boris Alexeev using Aristotle.

theorem erdos_505 : type_of% borsuk_conjecture.not_forall

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

Erdos505.erdos_505.small_dim

Solved: stated here without proof.

Borsuk's conjecture, small dimensions: Borsuk.BorsukConjecture n holds for \(n \leq 3\). Elementary for \(n \leq 1\), proved by Borsuk [Bo33] for \(n = 2\) and by Eggleston [Eg55] for \(n = 3\).

theorem erdos_505.small_dim (n : ℕ) (hn : n ≤ 3) : BorsukConjecture n

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

Sources

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

LeanErdos505.erdos_505 · Erdos505.erdos_505.small_dim

TheoremErdős Problem 506#

References: - erdosproblems.com/506 - [El67] Elliott, P. D. T. A., On the number of circles determined by \(n\) points, Acta Math. Acad. Sci. Hungar. (1967), 181–188. - [BaBa94] Bálintová, A. and Bálint, V., On the number of circles determined by \(n\) points in the Euclidean plane, Acta Math. Hungar. (1994), 283–289. - [PuSm] Purdy and Smith. No reference found.

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

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

Erdos506.erdos_506

Open: stated without proof.

What is the minimum number of circles determined by any \(n\) points in \(\mathbb{R}^2\), not all on a circle?

There is clearly some non-degeneracy condition intended here - probably either that not all the points are on a line, or the stronger condition that no three points are on a line.

The answer is known for \(n > 393\) (see erdos_506.variants.large_n) but the problem appears to remain open for small \(n\) (see erdos_506.variants.small_n).

theorem erdos_506 (n : ℕ) (hn : 4 ≤ n) :
    IsLeast { k : ℕ | ∃ P : Finset ℝ²,
        P.card = n ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
        numCircles (P : Set ℝ²) = k }
      erdos_506.answer

Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/506.lean, line 66.

Erdos506.erdos_506.variants.large_n

Solved: stated here without proof.

For \(n > 393\) the answer is \(\binom{n-1}{2} + 1 - \left\lfloor \frac{n-1}{2} \right\rfloor\) (Elliott [El67], with the correction of Purdy and Smith [PuSm], also reported in [BaBa94]): this is both a lower bound for every such configuration and is attained, e.g. by a circle with \(n - 1\) points together with a single point off the circle.

theorem erdos_506.variants.large_n (n : ℕ) (hn : 393 < n) :
    IsLeast { k : ℕ | ∃ P : Finset ℝ²,
        P.card = n ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
        numCircles (P : Set ℝ²) = k }
      (erdos_506.variants.large_n.answer n)

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/506.lean, line 82.

Erdos506.erdos_506.variants.small_n

Open: stated without proof.

The problem appears to remain open for small \(n\): Elliott's answer is established only for \(n > 393\), so the minimum number of circles determined by \(n\) points, not all on a line and not all on a circle, is unknown for \(n \le 393\).

theorem erdos_506.variants.small_n (n : ℕ) (hn : 4 ≤ n) (hn' : n ≤ 393) :
    IsLeast { k : ℕ | ∃ P : Finset ℝ²,
        P.card = n ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
        numCircles (P : Set ℝ²) = k }
      erdos_506.variants.small_n.answer

Category research open; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/506.lean, line 97.

Erdos506.erdos_506.variants.segre_n_eq_eight

Solved: stated here without proof.

Segre's observation: the lower bound \(\binom{n-1}{2}\) (without the correction of [PuSm]) is already false for \(n = 8\), as witnessed by the projection of a cube onto a plane. Hence the minimum number of circles determined by \(8\) such points is strictly less than \(\binom{7}{2} = 21\).

theorem erdos_506.variants.segre_n_eq_eight :
    ∃ P : Finset ℝ²,
      P.card = 8 ∧ ¬ Collinear ℝ (P : Set ℝ²) ∧ ¬ Cospherical (P : Set ℝ²) ∧
      numCircles (P : Set ℝ²) < (8 - 1).choose 2

Category research solved; AMS 51 Geometry, 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/506.lean, line 110.

Sources

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

LeanErdos506.erdos_506 · Erdos506.erdos_506.variants.large_n · Erdos506.erdos_506.variants.small_n · Erdos506.erdos_506.variants.segre_n_eq_eight

TheoremErdős Problem 507#

References: - erdosproblems.com/507 - [CPZ23] Cohen, Alex, Cosmin Pohoata, and Dmitrii Zakharov. "A new upper bound for the Heilbronn triangle problem." arXiv preprint arXiv:2305.18253 (2023). - [CPZ24] Cohen, Alex, Cosmin Pohoata, and Dmitrii Zakharov. "Lower bounds for incidences." Inventiones mathematicae (2025): 1-74. - [KPS82] Komlós, János, János Pintz, and Endre Szemerédi. "A lower bound for Heilbronn's problem." Journal of the London Mathematical Society 2.1 (1982): 13-24. - [KPS81] Komlós, János, János Pintz, and Endre Szemerédi. "On Heilbronn's triangle problem." Journal of the London Mathematical Society 2.3 (1981): 385-396.

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

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

Erdos507.erdos_507.equivalent

Open: stated without proof.

Let \(\alpha(n)\) be such that every set of \(n\) points in the unit disk contains three points which determine a triangle of area at most \(\alpha(n)\). Estimate \(\alpha(n)\).

theorem erdos_507.equivalent:
    α ~[atTop] erdos_507.equivalent.answer

Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 75.

Erdos507.erdos_507.lower

Open: stated without proof.

Estimate a lower bound for\(\alpha(n)\).

theorem erdos_507.lower:
    (lowerBest =o[atTop] erdos_507.lower.answer) ∧ (erdos_507.lower.answer ≪ α)

Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 85.

Erdos507.erdos_507.upper

Open: stated without proof.

Estimate an upper bound for\(\alpha(n)\).

theorem erdos_507.upper:
    (α ≪ erdos_507.upper.answer) ∧ (erdos_507.upper.answer =o[atTop] upperBarrier)

Category research open; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 95.

Erdos507.erdos_507.variants.upper_trivial

Solved: stated here without proof.

It is trivial that \(\alpha(n) \ll 1/n\).

theorem erdos_507.variants.upper_trivial : α ≪ (fun n ↦ 1 / (n : ℝ))

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 103.

Erdos507.erdos_507.variants.lower_erdos

Solved: stated here without proof.

Erdős observed that \(\alpha(n) \gg 1/n^2\).

theorem erdos_507.variants.lower_erdos : α ≫ (fun n ↦ 1 / (n : ℝ) ^ 2)

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 110.

Erdos507.erdos_507.variants.lower_kps82

Solved: stated here without proof.

Current best lower bound [KPS82].

theorem erdos_507.variants.lower_kps82 : lowerBest ≪ α

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 117.

Erdos507.erdos_507.variants.upper_cpz24

Solved: stated here without proof.

Current best upper bound [CPZ24]: \(\alpha(n) \ll n^{-7/6 + o(1)}\).

theorem erdos_507.variants.upper_cpz24 :
    ∃ (o : ℕ → ℝ), Tendsto o atTop (𝓝 0) ∧
    α ≪ (fun n ↦ upperBarrier n * (n : ℝ) ^ o n)

Category research solved; AMS 51 Geometry. Declared in FormalConjectures/ErdosProblems/507.lean, line 124.

Sources

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

LeanErdos507.erdos_507.equivalent · Erdos507.erdos_507.lower · Erdos507.erdos_507.upper · Erdos507.erdos_507.variants.upper_trivial · Erdos507.erdos_507.variants.lower_erdos · Erdos507.erdos_507.variants.lower_kps82 · Erdos507.erdos_507.variants.upper_cpz24

TheoremErdős Problem 508#

Reference: erdosproblems.com/508

proven by considering the [Moser-Spindel graph] or the [Golomb graph] At least 4 colors are required: Moser-Spindel graph At least 4 colors are required: Golomb graph At least 5 colors are required: de Grey 2018 At least 6 colors are required, and 7 colors suffice: [OAI26]

• [OAI26] OpenAI, The Euclidean plane is not five-colorable. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf

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

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

Erdos508.HadwigerNelsonProblem

Open: stated without proof.

The Hadwiger–Nelson problem asks: How many colors are required to color the plane such that no two points at distance 1 from each other have the same color?

It is known that \(6 \leq \chi(\mathbb{R}^2) \leq 7\); see HadwigerNelsonAtLeastSix and HadwigerNelsonAtMostSeven.

theorem HadwigerNelsonProblem :
    χ(ℝ²) = HadwigerNelsonProblem.answer

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

Erdos508.HadwigerNelsonAtLeastFive

Solved: stated here without proof.

Aubrey de Grey improved the lower bound for the chromatic number of the plane to 5 in 2018 using a graph that has >1000 nodes.

"The chromatic number of the plane is at least 5" Aubrey D. N. J. de Grey, 2018 (https://doi.org/10.48550/arXiv.1804.02385)

theorem HadwigerNelsonAtLeastFive :
    5 ≤ χ(ℝ²)

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

Erdos508.HadwigerNelsonAtLeastSix

Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Geometry/PlaneColoring/Five.lean#L124.

The chromatic number of the plane is at least 6: there is no proper 5-colouring of the plane.

This was proved by an internal OpenAI model in September 2026 [OAI26]; see the linked Lean proof.

theorem HadwigerNelsonAtLeastSix :
    6 ≤ χ(ℝ²)

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

Erdos508.HadwigerNelsonAtLeast4

Solved: stated here; a Lean proof is at https://github.com/anatoliiohorodnyk/lean-fc-proofs/blob/394ec1c1ff92bdf2fa10f30d62ae9d0455d3ce20/Proofs/T_Erdos508_HadwigerNelsonAtLeast4.lean#L88.

The "chromatic number of the plane" is at least 4. This can be proven by considering the Moser-Spindel graph or the Golomb graph graph.

theorem HadwigerNelsonAtLeast4 : 4 ≤ χ(ℝ²)

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

Erdos508.HadwigerNelsonAtMostSeven

Textbook result, stated without proof. A Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Geometry/PlaneColoring/Seven.lean#L36.

This upper bound for the chromatic number of the plane was observed by John R. Isbell. His approach was dividing the plane into hexagons of uniform size and coloring them with a repeating pattern. A proof can probably be found in:

Soifer, Alexander (2008), The Mathematical Coloring Book: Mathematics of Coloring and the Colorful Life of its Creators, New York: Springer, ISBN 978-0-387-74640-1

An alternative approach that uses square tiling was highlighted by László Székely.

The linked Lean proof of this bound is part of the OpenAI release [OAI26].

theorem HadwigerNelsonAtMostSeven :
    χ(ℝ²) ≤ 7

Category textbook; AMS 52 Convex and discrete geometry. Declared in FormalConjectures/ErdosProblems/508.lean, line 107.

Erdos508.HadwigerNelsonAtLeastThree

Textbook result, proved here.

The chromatic number of the plane is at least 3.

This is proven by considering an equilateral triangle in the plane.

theorem HadwigerNelsonAtLeastThree : 3 ≤ χ(ℝ²)

Category textbook; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/508.lean, line 115.

Sources

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

LeanErdos508.HadwigerNelsonProblem · Erdos508.HadwigerNelsonAtLeastFive · Erdos508.HadwigerNelsonAtLeastSix · Erdos508.HadwigerNelsonAtLeast4 · Erdos508.HadwigerNelsonAtMostSeven · Erdos508.HadwigerNelsonAtLeastThree

TheoremErdős Problem 509#

Reference: erdosproblems.com/509

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

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

Erdos509.erdos_509

Open: stated without proof.

Let \(f(z) ∈ ℂ[z]\) be a monic non-constant polynomial. Can the set \(\{z ∈ ℂ : |f(z)| ≤ 1\}\) be covered by a set of closed discs the sum of whose radii is \(≤ 2\)?

theorem erdos_509 : ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2 ι)

Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/509.lean, line 85.

Erdos509.erdos_509.variants.Cartan_bound

Solved: stated here without proof.

Let \(f(z) ∈ ℂ[z]\) be a monic non-constant polynomial. Can the set \(\{z ∈ ℂ : |f(z)| ≤ 1\}\) be covered by a set of closed discs the sum of whose radii is \(≤ 2e\)? Solution: True. This is due to Cartan. See Sur les systèmes de fonctions holomorphes à variétés linéaires lacunaires et leurs applications, Henri Cartan, http://www.numdam.org/article/ASENS_1928_3_45__255_0.pdf

theorem erdos_509.variants.Cartan_bound : ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} (2*rexp 1) ι)

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

Erdos509.erdos_509.variants.Pommerenke_bound

Solved: stated here without proof.

Let \(f(z) ∈ ℂ[z]\) be a monic non-constant polynomial. Can the set \(\{z ∈ ℂ : |f(z)| ≤ 1\}\) be covered by a set of closed discs the sum of whose radii is \(≤ 2.59\)? Solution: True. This is due to Pommerenke.

theorem erdos_509.variants.Pommerenke_bound : ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2.59 ι)

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

Erdos509.erdos_509.variants.Pommerenke_connected

Solved: stated here without proof.

Let \(f(z) ∈ ℂ[z]\) be a monic non-constant polynomial. If it is connected, can the set \(\{z ∈ ℂ : |f(z)| ≤ 1\}\) be covered by a set of circles the sum of whose radii is \(≤ 2\)? Solution: True. This is due to Pommerenke.

theorem erdos_509.variants.Pommerenke_connected : ∀ (f : ℂ[X]), f.Monic → f.natDegree ≠ 0 →
    IsConnected {z | ‖f.eval z‖ ≤ 1} →
    ∃ (ι : Type), Nonempty (BoundedDiscCover {z | ‖f.eval z‖ ≤ 1} 2 ι)

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

Sources

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

LeanErdos509.erdos_509 · Erdos509.erdos_509.variants.Cartan_bound · Erdos509.erdos_509.variants.Pommerenke_bound · Erdos509.erdos_509.variants.Pommerenke_connected

TheoremErdős Problem 510#

References: - erdosproblems.com/510 - Ben Green's Open Problem 81 - [Ru04] Ruzsa, Imre Z., Negative values of cosine sums. Acta Arith. (2004), 179-186. - [Be25c] B. Bedert, Polynomial bounds for the Chowla Cosine Problem. arXiv:2509.05260 (2025).

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

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

Erdos510.erdos_510

Open: stated without proof.

Chowla's cosine problem

If \(A\subset \mathbb{N}\) is a finite set of positive integers of size \(N > 0\) then is there some absolute constant \(c>0\) and \(\theta\) such that

\[\sum_{n\in A}\cos(n\theta) < -cN^{1/2}?\]

theorem erdos_510 :
    ∃ (c : ℝ) (hc : 0 < c),
      ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
      ∃ θ, ∑ n ∈ A, cos (n * θ) < -c * sqrt N

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

Erdos510.erdos_510.variants.ruzsa

Solved: stated here without proof.

Ruzsa [Ru04] proved an upper bound of \(-\exp(O(\sqrt{\log N})\).

theorem erdos_510.variants.ruzsa :
    ∃ (c : ℝ) (hc : 0 < c),
      ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
      ∃ θ, ∑ n ∈ A, cos (n * θ) < - exp (c * sqrt (log N))

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

Erdos510.erdos_510.variants.bedert

Solved: stated here without proof.

Bedert [Be25c] proved an upper bound of \(-c N^{1/7}\).

theorem erdos_510.variants.bedert :
    ∃ (c : ℝ) (hc : 0 < c),
      ∀ᶠ N in atTop, ∀ (A : Finset ℕ), 0 ∉ A → #A = N →
      ∃ θ, ∑ n ∈ A, cos (n * θ) < - c * N ^ (1 / 7 : ℝ)

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

Sources

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

LeanErdos510.erdos_510 · Erdos510.erdos_510.variants.ruzsa · Erdos510.erdos_510.variants.bedert

TheoremErdős Problem 512#

References: - erdosproblems.com/512 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Ko81] Konyagin, S. V., On the Littlewood problem. Izv. Akad. Nauk SSSR Ser. Mat. (1981), 243-265, 463. - [MPS81] McGehee, O. Carruth and Pigno, Louis and Smith, Brent, Hardy's inequality and the \(L^1\) norm of exponential sums. Ann. of Math. (2) (1981), 613-618.

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

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

Erdos512.erdos_512

Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/f8a51976fd2e66a52b4928c109fb9ae877a1a507/problems/512/Erdos512.lean.

Is it true that, if \(A\subset \mathbb{Z}\) is a finite set of size \(N\), then

\[\int_0^1 \left\lvert \sum_{n\in A}e(n\theta)\right\rvert \mathrm{d}\theta \gg \log N,\]

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

Littlewood's conjecture, proved independently by Konyagin [Ko81] and McGehee, Pigno, and Smith [MPS81].

theorem erdos_512 :
    ∃ c > (0 : ℝ), ∀ (N : ℕ) (A : Finset ℤ), A.card = N →
      c * Real.log N ≤ ∫ θ in (0 : ℝ)..1, ‖∑ n ∈ A, e (n * θ)‖

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

Sources

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

LeanErdos512.erdos_512

TheoremErdős Problem 513#

Reference: - erdosproblems.com/513 - [ClHa64] Clunie, J. and Hayman, W. K., The maximum term of a power series. J. Analyse Math. (1964), 143-186. - Tao's optimization constant 51a

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

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

Erdos513.erdos_513

Open: stated without proof.

Let f be a transcendental entire function. What is the greatest possible value of liminf (fun r : ℝ => ratio r f) atTop?

theorem erdos_513 : maxTermConstant = erdos_513.answer

Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/513.lean, line 53.

Erdos513.erdos_513.variants.upper_bound

Solved: stated here without proof.

There is c > 0 such that maxTermConstant ≤ 2 / π - c. This is proved in [ClHa64].

theorem erdos_513.variants.upper_bound : ∃ c > 0, maxTermConstant ≤ 2 / π - c

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

Erdos513.erdos_513.variants.lower_bound

Solved: stated here without proof.

maxTermConstant > 1 / 2: there is a transcendental entire f with liminf (fun r : ℝ => ratio r f) atTop > 1 / 2. This was observed by Kövári (unpublished), and [ClHa64] proves the stronger bound > 4 / 7. It does not hold for every f: for f = exp the liminf is 0.

theorem erdos_513.variants.lower_bound : maxTermConstant > 1 / 2

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

Sources

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

LeanErdos513.erdos_513 · Erdos513.erdos_513.variants.upper_bound · Erdos513.erdos_513.variants.lower_bound

TheoremErdős Problem 516#

References: - erdosproblems.com/516 - [Fu63] Fuchs, W. H. J., Proof of a conjecture of G. Pólya concerning gap series. Illinois J. Math. (1963), 661--667. - [Ko65] Kövari, Thomas, A gap-theorem for entire functions of infinite order. Michigan Math. J. (1965), 133--140. - [Ki26] Kitamura, Kenta, A Lean counterexample to the Fejér-gap variant of Erdős Problem 516. GitHub (2026).

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

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

Erdos516.erdos_516

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

Let f = ∑ aₖzⁿₖ be an entire function of finite order such that nₖ / k → ∞. Then limsup (fun r => ratio r f) atTop = 1. This is proved in [Fu63].

theorem erdos_516 {f : ℂ → ℂ} {n : ℕ → ℕ}
    (hn : HasFabryGaps n) {a : ℕ → ℂ} (ha : ∀ n, a n ≠ 0)
    (hfn : ∀ z, HasSum (fun k => a k * z ^ n k) (f z)) (hf : OfFiniteOrder f) :
    limsup (fun r => ratio r f) atTop = 1

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

Erdos516.erdos_516.variants.limsup_ratio_eq_one

Solved: stated here without proof.

Let f = ∑ aₖzⁿₖ be an entire function with strictly increasing exponents such that nₖ > k (log k) ^ (2 + c). Then limsup (fun r => ratio r f) atTop = 1. This is proved in [Ko65]. Without StrictMono n, repeated exponents let nonzero coefficients cancel, and f = 0 satisfies the other hypotheses.

theorem erdos_516.variants.limsup_ratio_eq_one {f : ℂ → ℂ} {n : ℕ → ℕ} (hmono : StrictMono n)
    (hn : ∃ c > (0 : ℝ), ∀ k, n k > k * log k ^ (2 + c)) {a : ℕ → ℂ} (ha : ∀ n, a n ≠ 0)
    (hfn : ∀ z, HasSum (fun k => a k * z ^ n k) (f z)) :
    limsup (fun r => ratio r f) atTop = 1

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

Erdos516.erdos_516.variants.limsup_ratio_eq_one_of_hasFejerGaps

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-516-fejer-counterexample/blob/675d078d1c9fee4fcaa1c1a2eecde1c174853ff5/lean/Erdos516FejerFC.lean#L1304-L1314.

Is it true that for all entire functions f = ∑ aₖzⁿₖ such that ∑' 1 / nₖ < ∞, limsup (fun r => ratio r f) atTop = 1?

The answer is no: [Ki26] gives an explicit counterexample whose limsup is not 1.

theorem erdos_516.variants.limsup_ratio_eq_one_of_hasFejerGaps :
    ¬ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ} (hn : HasFejerGaps n) {a : ℕ → ℂ} (ha : ∀ n, a n ≠ 0)
    (hfn : ∀ z, HasSum (fun k => a k * z ^ n k) (f z)),
    limsup (fun r => ratio r f) atTop = 1

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

Sources

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

LeanErdos516.erdos_516 · Erdos516.erdos_516.variants.limsup_ratio_eq_one · Erdos516.erdos_516.variants.limsup_ratio_eq_one_of_hasFejerGaps

TheoremErdős Problem 517#

References: - erdosproblems.com/517 - [Bi28] Biernacki, Miécislas, Sur les équations algébriques contenant des paramétres arbitraires. (1928), 145.

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

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

Erdos517.erdos_517

Open: stated without proof.

If f(z) = ∑ aₖzⁿₖ is an entire function (with aₖ ≠ 0 for all k) such that nₖ / k → ∞, is it true that f assumes every value infinitely often?

theorem erdos_517 : ∀ {f : ℂ → ℂ} {n : ℕ → ℕ} (hn : HasFabryGaps n)
    {a : ℕ → ℂ} (ha : ∀ k, a k ≠ 0) (hf : ∀ z, HasSum (fun k => a k * z ^ n k) (f z)) (z : ℂ),
    {x : ℂ | f x = z}.Infinite

Category research open; AMS 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/517.lean, line 38.

Erdos517.erdos_517.variants.fejer

Solved: stated here without proof.

If f(z) = ∑ aₖzⁿₖ is an entire function (with aₖ ≠ 0 for all k) such that ∑ 1 / nₖ < ∞, then f assumes every value infinitely often. This theorem is proved in [Bi28].

theorem erdos_517.variants.fejer {f : ℂ → ℂ} {n : ℕ → ℕ} (hn : HasFejerGaps n) {a : ℕ → ℂ}
    (ha : ∀ k, a k ≠ 0) (hf : ∀ z, HasSum (fun k => a k * z ^ n k) (f z)) (z : ℂ) :
    {x : ℂ | f x = z}.Infinite

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

Sources

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

LeanErdos517.erdos_517 · Erdos517.erdos_517.variants.fejer

TheoremErdős Problem 519#

References: - erdosproblems.com/519 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244. - [Bi94] Biró, A., On a problem of Turán concerning sums of powers of complex numbers. Acta Math. Hungar. (1994), 209-216. - [Bi00] Biró, András, An improved estimate in a power sum problem of Turán. Indag. Math. (N.S.) (2000), 343-358. - [Bi00b] Biró, A., An upper estimate in Turán's pure power sum problem. Indag. Math. (N.S.) (2000), 499--508. - [At61b] Atkinson, F. V., On sums of powers of complex numbers. Acta Math. Acad. Sci. Hungar. (1961), 185-188.

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

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

Erdos519.erdos_519

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

Let \(z_1,\ldots,z_n\in \mathbb{C}\) with \(z_1=1\). Must there exist an absolute constant \(c>0\) such that

\[ \max_{1\leq k\leq n}\left\lvert \sum_{i}z_i^k\right\rvert>c? \]

Atkinson proved that \(c=1/6\) suffices.

theorem erdos_519 :
    ∃ c : ℝ, 0 < c ∧
      ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ),
        z ⟨0, hn⟩ = 1 →
          ∃ k : Fin n, c < ‖powerSum z (k.val + 1)‖

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

Sources

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

LeanErdos519.erdos_519

TheoremErdős Problem 520#

References: - erdosproblems.com/520 - [Hø26] Høystad, S. W. R., A self-contained Lean 4 proof that Erdős Problem #520 has a negative answer (2026), https://github.com/saasom/Erdos520/blob/v1.1.0/paper/erdos520_note.pdf - [Ha13] Harper, A. J., Bounds on the suprema of Gaussian processes, and omega results for the sum of a random multiplicative function. Ann. Appl. Probab. 23 (2013), 584–616.

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

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

Erdos520.erdos_520

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

Let \(f\) be a Rademacher multiplicative function. Does there exist some constant \(c > 0\) such that, almost surely,

\[ \limsup_{N \to \infty} \frac{\sum_{m \leq N} f(m)}{\sqrt{N \log \log N}} = c? \]

The answer is no: Høystad [Hø26] (with GPT-5.6 Pro and Claude) proved, following the Halász–Lau–Tenenbaum–Wu–Caich martingale approach with Harper's low-moment estimates [Ha13], that almost surely \(\sum_{m \le N} f(m) \ll \sqrt{N} (\log \log N)^{1/4 + \eta}\) for every \(\eta > 0\), so the \(\limsup\) is \(0\) almost surely. The linked formal proof works with the concrete model ℕ → Bool with the product of fair coins, whose squarefree-supported Rademacher function is IsRademacherMultiplicative; this refutes the statement below.

theorem erdos_520 :
    ¬ ∃ c > 0, ∀ (Ω : Type) [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
      (f : ℕ → Ω → ℝ), IsRademacherMultiplicative f →
      ∀ᵐ ω, limsup (fun N ↦ ∑ m ≤ N, f m ω / sqrt (N * log (log N))) atTop = c

Category research solved; AMS 11 Number theory, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/520.lean, line 75.

Sources

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

LeanErdos520.erdos_520

TheoremErdős Problem 521#

Reference: erdosproblems.com/521

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

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

Erdos521.erdos_521

Solved: stated here; a Lean proof is at https://github.com/williamjblair/lean-proofs/blob/4f915a323443bfb1709a6805a013812016dca88a/starfleet/erdos-521/Research/LateFourthFinal.lean.

Let \((\epsilon_k)_{k\geq 0}\) be independently uniformly chosen at random from \(\{-1,1\}\). If \(R_n\) counts the number of real roots of \(f_n(z)=\sum_{0\leq k\leq n}\epsilon_k z^k\) then is it true that, almost surely,

\[\lim_{n\to \infty}\frac{R_n}{\log n}=\frac{2}{\pi}?\]

The answer is no: this almost-sure limit fails. This result was obtained first by others, who deserve the credit for the problem; the link is to an independent machine-checked proof by Star Fleet Math.

theorem erdos_521 : ¬ Claim

Category research solved; AMS 11 Number theory, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/521.lean, line 85.

Sources

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

LeanErdos521.erdos_521

TheoremErdős Problem 522#

References: - erdosproblems.com/522 - [Ch26] Chojecki, P., A strong law for the roots of random Littlewood polynomials (2026), ulam.ai/research/erdos522-final.pdf. - [Ka26] Kawada, S., Almost-Sure Radial Laws for Nested Random Polynomials and Erdős Problem #522, doi:10.5281/zenodo.22970145 (2026). Lean 4 formalization: chreia/erdos-522. - [Ki26] Kitamura, K., A Lean proof of Erdős Problem 522, KitaKen1/erdos-522-strong-law (2026). - [KZ26] Kwon, Y. and Zou, J., A fourth moment estimate for logarithmic integrals of random Littlewood polynomials and Erdős's root-count problem (2026), ykwon0407/erdos-521-522.

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

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

Erdos522.erdos_522

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-522-strong-law/blob/9374493206d192708ef50f90f2752aa0dc690e16/lean/Erdos522StrongLawFC.lean#L9086-L9089; a Lean proof is at https://github.com/chreia/erdos-522/blob/b3c1d7c089fcada59cc48cf664cd3d02157407ca/lean/Erdos522/Probability/IndependentCoefficientRadialLaws.lean#L39-L47; a Lean proof is at https://github.com/chreia/erdos-522/blob/57af1556d1b40f37d09d1270495acc0f282ff0fc/lean/Erdos522/Bridge/FormalConjectures.lean#L238-L253.

Let \(f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k\) be a random polynomial, where \(\epsilon_k\in \{-1,1\}\) independently uniformly at random for \(0\leq k\leq n\).

Is it true that, if \(R_n\) is the number of roots of \(f(z)\) in \(\{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}\), then

\[ \frac{R_n}{n/2}\to 1 \]

almost surely?

There is some ambiguity as to whether the intended coefficient set is \(\{-1, 1\}\) or \(\{0, 1\}\), see erdos_522.variants.zero_one for the alternate version.

This is true. Proofs were posted on the erdosproblems.com forum in April 2026 [Ch26], [KZ26], and Lean proofs were given independently in September 2026 [Ka26], [Ki26].

More generally, [Ka26] proves an almost-sure radial law: the number of roots in \(\{\lvert z\rvert \le 1 + x/n\}\) is \(\Phi(x)\,n + o(n)\) for every \(x\), where \(\Phi(x) = \tfrac12\left(1 + \coth x - \tfrac1x\right)\). This problem is the case \(x = 0\).

theorem erdos_522 :
    ∀ {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
      (c : KacCoefficients ({-1, 1} : Set ℂ) Ω),
      ℙ {ω | atTop.Tendsto (fun n : ℕ ↦ (2 * c.numRootsInUnitDisk n ω : ℝ) / n) (𝓝 1)} = 1

Category research solved; AMS 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/522.lean, line 127.

Erdos522.erdos_522.variants.zero_one

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-522-strong-law/blob/9374493206d192708ef50f90f2752aa0dc690e16/lean/Erdos522StrongLawFC.lean#L9101-L9104.

Let \(f(z)=\sum_{0\leq k\leq n} \epsilon_k z^k\) be a random polynomial, where \(\epsilon_k\in \{0,1\}\) independently uniformly at random for \(0\leq k\leq n\).

Is it true that, if \(R_n\) is the number of roots of \(f(z)\) in \(\{ z\in \mathbb{C} : \lvert z\rvert \leq 1\}\), then

\[ \frac{R_n}{n/2}\to 1 \]

almost surely?

This is true; a Lean proof is given in [Ki26].

theorem erdos_522.variants.zero_one :
    ∀ {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
      {n : ℕ} (hn : 1 ≤ n) (f : KacCoefficients ({0, 1} : Set ℂ) Ω),
      ℙ {ω | atTop.Tendsto (fun n : ℕ ↦ (2 * f.numRootsInUnitDisk n ω : ℝ) / n) (𝓝 1)} = 1

Category research solved; AMS 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/522.lean, line 150.

Erdos522.erdos_522.variants.number_real_roots

Solved: stated here without proof.

Erdős and Offord showed that the number of real roots of a random degree n polynomial with ±1 coefficients is (2/π+o(1))log n.

theorem erdos_522.variants.number_real_roots : ∃ p o : ℕ → ℝ,
    atTop.Tendsto o (𝓝 0) ∧ atTop.Tendsto p (𝓝 0) ∧
    ∀ (Ω : Type*) [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
      (n : ℕ) (hn : 2 ≤ n) (f : KacCoefficients ({-1, 1} : Set ℝ) Ω),
      (ℙ {ω | |(f.roots n ω).card / (n : ℝ).log - 2 / π| ≥ o n}).toReal ≤ p n

Category research solved; AMS 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/522.lean, line 161.

Erdos522.erdos_522.variants.yakir_solution

Solved: stated here without proof.

Yakir proved that almost all Kac polynomials have n/2+O(n^(9/10)) many roots in {z∈C:|z|≤1}.

theorem erdos_522.variants.yakir_solution :
    ∃ p : ℕ → ℝ, atTop.Tendsto p (𝓝 0) ∧
    ∀ (Ω : Type*) [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
      (n : ℕ) (hn : 2 ≤ n) (f : KacCoefficients ({-1, 1} : Set ℂ) Ω),
       (ℙ {ω | |(f.roots n ω).countP
         (· ∈ Metric.closedBall 0 1) - (n / 2 : ℝ)| ≥ n^(9/10 : ℝ) }).toReal ≤ p n

Category research solved; AMS 12 Field theory and polynomials, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/522.lean, line 173.

Sources

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

LeanErdos522.erdos_522 · Erdos522.erdos_522.variants.zero_one · Erdos522.erdos_522.variants.number_real_roots · Erdos522.erdos_522.variants.yakir_solution

TheoremErdős Problem 525#

References: - erdosproblems.com/525 - [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254. - [Li66] Littlewood, J. E., On polynomials \(\sum^n \pm z^m\), \(\sum^n e^{\alpha_m i} z^m\), \(z = e^{\theta i}\). J. London Math. Soc. (1966), 367-376. - [Ka87] Kashin, B. S., The properties of random trigonometric polynomials with \(\pm 1\) coefficients. Vestnik Moskov. Univ. Ser. I Mat. Mekh. (1987), 40-46, 105. - [Ko94] Konyagin, S. V., On the minimum modulus of random trigonometric polynomials with coefficients \(\pm1\). Mat. Zametki (1994), 80-101, 158. - [KoSc99] Konyagin, S. V. and Schlag, W., Lower bounds for the absolute value of random polynomials on a neighborhood of the unit circle. Trans. Amer. Math. Soc. (1999), 4963-4980. - [CoNg21] Cook, Nicholas A. and Nguyen, Hoi H., Universality of the minimum modulus for random trigonometric polynomials. Discrete Anal. (2021), Paper No. 20, 46.

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

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

Erdos525.erdos_525.parts.i

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

Is it true that all except at most \(o(2^n)\) many degree \(n\) polynomials with \(\pm 1\)-valued coefficients \(f(z)\) have \(\lvert f(z)\rvert <1\) for some \(\lvert z\rvert=1\)?

The answer is yes: Littlewood [Li66] conjectured the stronger \(m(f)=o(1)\) almost surely, which was proved by Kashin [Ka87].

theorem erdos_525.parts.i :
    (fun n : ℕ ↦ ((exceptional n).ncard : ℝ)) =o[atTop] fun n : ℕ ↦ (2 : ℝ) ^ n

Category research solved; AMS 30 Functions of a complex variable, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/525.lean, line 75.

Erdos525.erdos_525.parts.ii

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

What is the behaviour of

\[m(f)=\min_{\lvert z\rvert=1}\lvert f(z)\rvert?\]

Cook and Nguyen [CoNg21] have identified the limiting distribution, proving that for any \(\epsilon>0\)

\[\lim_{n\to \infty} \mathbb{P}(m(f) > \epsilon n^{-1/2}) = e^{-\epsilon \lambda}\]

where \(\lambda=\sqrt{\pi/12}\).

theorem erdos_525.parts.ii (ε : ℝ) (hε : 0 < ε) :
    Tendsto (fun n : ℕ ↦ prob n fun f ↦ ε / √n < m f) atTop
      (nhds (exp (-√(π / 12) * ε)))

Category research solved; AMS 30 Functions of a complex variable, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/525.lean, line 91.

Erdos525.erdos_525.variants.kashin

Solved: stated here without proof.

Littlewood [Li66] conjectured that \(m(f)=o(1)\) holds almost surely; this was proved by Kashin [Ka87].

theorem erdos_525.variants.kashin (δ : ℝ) (hδ : 0 < δ) :
    Tendsto (fun n : ℕ ↦ prob n fun f ↦ m f < δ) atTop (nhds 1)

Category research solved; AMS 30 Functions of a complex variable, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/525.lean, line 99.

Erdos525.erdos_525.variants.konyagin

Solved: stated here without proof.

Konyagin [Ko94] proved that \(m(f)\leq n^{-1/2+o(1)}\) almost surely.

theorem erdos_525.variants.konyagin (δ : ℝ) (hδ : 0 < δ) :
    Tendsto (fun n : ℕ ↦ prob n fun f ↦ m f ≤ (n : ℝ) ^ (-1 / 2 + δ : ℝ)) atTop
      (nhds 1)

Category research solved; AMS 30 Functions of a complex variable, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/525.lean, line 105.

Erdos525.erdos_525.variants.konyagin_schlag

Solved: stated here without proof.

Konyagin and Schlag [KoSc99] proved that for any \(\epsilon>0\)

\[\limsup_{n\to \infty} \mathbb{P}(m(f) \leq \epsilon n^{-1/2})\ll \epsilon.\]

theorem erdos_525.variants.konyagin_schlag :
    ∃ C : ℝ, ∀ ε : ℝ, 0 < ε →
      limsup (fun n : ℕ ↦ prob n fun f ↦ m f ≤ ε / √n) atTop ≤ C * ε

Category research solved; AMS 30 Functions of a complex variable, 60 Probability theory and stochastic processes. Declared in FormalConjectures/ErdosProblems/525.lean, line 113.

Sources

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

LeanErdos525.erdos_525.parts.i · Erdos525.erdos_525.parts.ii · Erdos525.erdos_525.variants.kashin · Erdos525.erdos_525.variants.konyagin · Erdos525.erdos_525.variants.konyagin_schlag

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.