Erdős Problem 1128 to Erdős Problem 1157
TheoremErdős Problem 1128#
Reference: erdosproblems.com/1128
Quoted from FormalConjectures/ErdosProblems/1128.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/1128.
The file states 4 research or textbook statements: 4 solved.
Erdos1128.erdos_1128.prikryMills
Solved: stated here without proof.
Prikry–Mills counterexample (key lemma):
There exists a 2-colouring \(f\) of a set of cardinality \(\aleph_1\) cubed such that no countable box \(A_1 \times B_1 \times C_1\) is monochromatic.
This is the unpublished result of Prikry and Mills (1978). The proof proceeds by transfinite induction along \(\omega_1\), which has uncountable cofinality, ensuring every countable box is non-monochromatic.
theorem erdos_1128.prikryMills :
∃ (X : Type) (_ : #X = aleph 1) (f : X → X → X → Fin 2),
∀ (A₁ B₁ C₁ : Set X),
#A₁ = aleph 0 → #B₁ = aleph 0 → #C₁ = aleph 0 →
¬ IsMonochromaticBox f A₁ B₁ C₁
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1128.lean, line 106.
Erdos1128.erdos_1128
Proved here.
Erdős Problem 1128 (disproved by Prikry–Mills, 1978):
Erdős asked whether every 2-colouring of \(A \times B \times C\), where \(|A| = |B| = |C| = \aleph_1\), must contain a monochromatic countable box \(A_1 \times B_1 \times C_1\) with \(|A_1| = |B_1| = |C_1| = \aleph_0\).
The answer is No: Prikry and Mills constructed a 2-colouring of \(\omega_1^3\) with no monochromatic countable box.
Note: The positive statement asserts that every 2-colouring of every \(\aleph_1^3\) contains a monochromatic countably infinite box. Since the answer is False, this positive statement fails.
theorem erdos_1128 :
¬ ∀ (A B C : Type) (_ : #A = aleph 1) (_ : #B = aleph 1) (_ : #C = aleph 1)
(f : A → B → C → Fin 2),
∃ (A₁ : Set A) (B₁ : Set B) (C₁ : Set C),
#A₁ = aleph 0 ∧ #B₁ = aleph 0 ∧ #C₁ = aleph 0 ∧
IsMonochromaticBox f A₁ B₁ C₁
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1128.lean, line 151.
Erdos1128.erdos_1128.variants.prikryMills_explicit
Solved: stated here without proof.
Explicit form of Prikry–Mills:
There exists a 2-colouring of \(\omega_1 \times \omega_1 \times \omega_1\) such that for every countably infinite \(A_1, B_1, C_1 \subseteq \omega_1\), the box \(A_1 \times B_1 \times C_1\) is not monochromatic.
This is the content of the Prikry–Mills theorem (1978, unpublished), stated using Lean's ordinal type
{o : Ordinal // o < ω_ 1}as the representation of \(\omega_1\).
theorem erdos_1128.variants.prikryMills_explicit :
∃ (f : {o : Ordinal // o < ω_ 1} →
{o : Ordinal // o < ω_ 1} →
{o : Ordinal // o < ω_ 1} → Fin 2),
∀ (A₁ B₁ C₁ : Set {o : Ordinal // o < ω_ 1}),
#A₁ = aleph 0 → #B₁ = aleph 0 → #C₁ = aleph 0 →
¬ IsMonochromaticBox f A₁ B₁ C₁
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1128.lean, line 181.
Erdos1128.erdos_1128.variants.two_dimensional_false
Proved here.
The claim that every 2-colouring of \(\omega_1 \times \omega_1\) has an uncountable monochromatic product rectangle is false in ZFC.
Counterexample: The ordering colouring \(f(\alpha, \beta) = 0\) iff \(\alpha < \beta\) has no uncountable monochromatic product rectangle \(A_1 \times B_1\).
Proof: If \(A_1 \times B_1\) were monochromatic with colour 0, then every element of \(A_1\) would be strictly less than every element of \(B_1\), making \(A_1\) bounded above in \(\omega_1\); but any bounded subset of \(\omega_1\) is countable (since initial segments are countable), contradicting \(A_1\) being uncountable. The colour-1 case is symmetric with the roles of \(A_1\) and \(B_1\) swapped.
Note: For 2-colourings of unordered pairs the analogous statement also fails: Sierpiński showed \(\omega_1 \not\to (\omega_1)^2_2\). The Erdős–Rado theorem gives \((2^{\aleph_0})^+ \to (\aleph_1)^2_{\aleph_0}\) instead.
theorem erdos_1128.variants.two_dimensional_false :
¬ ∀ (f : Omega1 → Omega1 → Fin 2),
∃ (A₁ B₁ : Set Omega1),
¬ A₁.Countable ∧ ¬ B₁.Countable ∧
∃ c : Fin 2, ∀ a ∈ A₁, ∀ b ∈ B₁, f a b = c
Category research solved; AMS 03 Mathematical logic and foundations, 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1128.lean, line 231.
Sources
TheoremErdős Problem 1133#
References: - erdosproblems.com/1133 - [Er67] Erdős, P., Problems and results on the convergence and divergence properties of the Lagrange interpolation polynomials and some extremal problems. Mathematica (Cluj) (1967), 65-73. - [Ya26] Yang, J.-Q., Erdős's Robust Polynomial Interpolation Problem: the Optimal Exponential Scale. arXiv:2609.14769 (2026).
Quoted from FormalConjectures/ErdosProblems/1133.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/1133.
The file states 2 research or textbook statements: 2 solved.
Erdos1133.erdos_1133
Solved: stated here without proof.
Let \(C>0\). There exists \(\epsilon>0\) such that if \(n\) is sufficiently large the following holds.
For any \(x_1,\ldots,x_n\in [-1,1]\) there exist \(y_1,\ldots,y_n\in [-1,1]\) such that, if \(P\) is a polynomial of degree \(m<(1+\epsilon)n\) with \(P(x_i)=y_i\) for at least \((1-\epsilon)n\) many \(1\leq i\leq n\), then
\[\max_{x\in [-1,1]}\lvert P(x)\rvert >C.\]Yang [Ya26, Theorem 2.1] proved this, including repeated nodes, by taking \(\rho=0\).
theorem erdos_1133 :
∀ C > (0 : ℝ), ∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
∀ x : Fin n → Icc (-1 : ℝ) 1,
∃ y : Fin n → Icc (-1 : ℝ) 1,
∀ P : Polynomial ℝ,
(P.natDegree : ℝ) < (1 + ε) * (n : ℝ) →
((Finset.univ.filter (fun i ↦ P.eval (x i : ℝ) = (y i : ℝ))).card : ℝ) ≥
(1 - ε) * (n : ℝ) →
∃ z ∈ Icc (-1 : ℝ) 1, |P.eval z| > C
Category research solved; AMS 26 Real functions, 41 Approximations and expansions. Declared in FormalConjectures/ErdosProblems/1133.lean, line 47.
Erdos1133.erdos_1133.variants.weaker
Solved: stated here without proof.
Erdős proved that, for any \(C>0\), there exists \(\epsilon>0\) such that if \(n\) is sufficiently large and \(m=\lfloor (1+\epsilon)n\rfloor\) then for any \(x_1,\ldots,x_m\in [-1,1]\) there is a polynomial \(P\) of degree \(n\) such that \(\lvert P(x_i)\rvert\leq 1\) for \(1\leq i\leq m\) and \(\max_{x\in [-1,1]}\lvert P(x)\rvert>C\). The robust interpolation statement above also implies this result. Erdős in [Er67] could not prove the robust statement even for \(m=n\).
theorem erdos_1133.variants.weaker :
∀ C > (0 : ℝ), ∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,
let m := ⌊(1 + ε) * (n : ℝ)⌋₊;
∀ x : Fin m → Icc (-1 : ℝ) 1,
∃ P : Polynomial ℝ,
P.natDegree = n ∧
(∀ i : Fin m, |P.eval (x i : ℝ)| ≤ 1) ∧
∃ z ∈ Icc (-1 : ℝ) 1, |P.eval z| > C
Category research solved; AMS 26 Real functions, 41 Approximations and expansions. Declared in FormalConjectures/ErdosProblems/1133.lean, line 66.
Sources
TheoremErdős Problem 1134#
References: - erdosproblems.com/1134 - [La16] Lagarias, Jeffrey C., Erdős, Klarner, and the \(3x+1\) problem. Amer. Math. Monthly (2016), 753--776. - [KlRa74] Klarner, D. A. and Rado, R., Arithmetic properties of certain recursively defined sets. Pacific J. Math. (1974), 445--463. - [Kl82] Klarner, David A., A sufficient condition for certain semigroups to be free. J. Algebra (1982), 140--148. - [Gu83b] Guy, Richard K., Unsolved Problems: Don't Try to Solve These Problems. Amer. Math. Monthly (1983), 35--38+39--41. - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
Quoted from FormalConjectures/ErdosProblems/1134.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/1134.
The file states 3 research or textbook statements: 3 solved.
Erdos1134.erdos_1134
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1134.lean#L79.
Let \(A\subseteq \mathbb{N}\) be the smallest set which contains \(1\) and is closed under the operations
\[x\mapsto 2x+1,\quad x\mapsto 3x+1,\quad x\mapsto 6x+1.\]Does \(A\) have positive lower density?
Lagarias [La16] reports that Erdős asked this in 1972, offering £10 for a solution. (Although Hilton told Lagarias that this problem may have been formulated by Klarner, and that Erdős liked it and offered a prize for its solution.)
Erdős had earlier proved (as reported in [KlRa74]) that if \(A\) is the smallest set which contains \(1\) and is closed under the operations \(x\mapsto m_ix+b_i\) for some (possibly infinite) collection of \(m_i\geq 1\) and \(b_i\geq 0\) then, if \(\sigma>0\) is such that \(\sum \frac{1}{m_i^\sigma}=1\) then, for all large \(X\), \(\lvert A\cap [1,X]\rvert \ll X^{\sigma+o(1)}\). This result does not help with the given problem since \(\frac{1}{2}+\frac{1}{3}+\frac{1}{6}=1\).
This was answered in the negative soon afterwards by Crampin and Hilton (as reported in [Kl82]), who proved that in fact, for all large \(X\), \(\lvert A\cap [1,X]\rvert \ll X^{\tau+o(1)}\) where \(\tau\approx 0.900626\) is the unique positive root of
\[6^{-\tau}+\sum_{k\geq 0}(3\cdot 2^k)^{-\tau}=1.\]Their proof is given in [La16]. This problem is repeated by Guy [Gu83b] in an article called 'Don't Try to Solve These Problems'. This is Problem E36 in Guy's collection [Gu04].
theorem erdos_1134 : ¬ 0 < A.lowerDensity
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1134.lean, line 71.
Erdos1134.erdos_1134.variants.sublinear
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1134/Dirichlet.lean#L376.
The counting function of \(A\) is sublinear: \(\lvert A\cap [1,X]\rvert \ll X^{\tau+o(1)}\) with \(\tau < 1\), so in particular \(\lvert A \cap [1, X]\rvert \ll X^{19/20}\).
theorem erdos_1134.variants.sublinear :
∃ C : ℝ, 0 < C ∧ ∀ X : ℕ, ((A ∩ Set.Iic X).ncard : ℝ) ≤ C * (X : ℝ) ^ (19 / 20 : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1134.lean, line 79.
Erdos1134.erdos_1134.variants.klarner
Solved: stated here; a Lean proof is at https://github.com/KitaKen1/erdos-1134-lean/blob/57042c7e43ae71cd7008e461cf3b9d81b8d8a20f/lean/Erdos1134KlarnerFC.lean#L2110-L2113.
Klarner has several (open) variants of this problem - see Section 8.9 of [La16]. For example, it is unknown if the smallest set \(A\) which contains \(0\) and is closed under
\[x\mapsto 2x,\quad x\mapsto 3x+2,\quad x\mapsto 6x+3\]has positive density.
The answer is negative: Kenta Kitamura (KitaKen1 on GitHub) has given a Lean proof (erdos-1134-lean) that \(A\) has natural density \(0\).
theorem erdos_1134.variants.klarner :
¬ 0 < (⋂₀ {S : Set ℕ | 0 ∈ S ∧
∀ x ∈ S, 2 * x ∈ S ∧ 3 * x + 2 ∈ S ∧ 6 * x + 3 ∈ S}).lowerDensity
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1134.lean, line 95.
Sources
TheoremErdős Problem 1135#
The Collatz conjecture states that for any positive integer \(n\), there exists a natural number \(m\) such that the \(m\)-th term of the sequence is 1.
References: - erdosproblems.com/1135 - [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437. - [La10] Lagarias, Jeffrey C., The {\(3x+1\)} problem: an overview. (2010), 3--29. - [La16] Lagarias, Jeffrey C., Erdős, Klarner, and the {\(3x+1\)} problem. Amer. Math. Monthly (2016), 753--776. - [La85] Lagarias, Jeffrey C., The {\(3x+1\)} problem and its generalizations. Amer. Math. Monthly (1985), 3--23.
This file points to the canonical formalization in
FormalConjectures.Wikipedia.CollatzConjecture.
Quoted from FormalConjectures/ErdosProblems/1135.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/1135.
The file states 1 research or textbook statement: 1 open.
Erdos1135.erdos_1135
Open: stated without proof.
The Collatz conjecture states that for any positive integer \(n\), there exists a natural number \(m\) such that the \(m\)-th term of the sequence is 1.
theorem erdos_1135 : type_of% CollatzConjecture.collatz_conjecture
Category research open; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/ErdosProblems/1135.lean, line 47.
Sources
TheoremErdős Problem 1136#
References: - erdosproblems.com/1136 - [Mu11] Müller, Helmut, Über ein additiv-zahlentheoretisches Problem von P. Erdős. Mitt. Math. Ges. Hamburg (2011), 75-78.
Quoted from FormalConjectures/ErdosProblems/1136.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/1136.
The file states 4 research or textbook statements: 4 solved.
Erdos1136.erdos_1136
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos1136.lean.
Does there exist \(A\subset \mathbb{N}\) with lower density \(>1/3\) such that \(a+b\neq 2^k\) for any \(a,b\in A\) and \(k\geq 0\)?
Müller [Mu11] settled this question in the affirmative: in fact one can take \(A\) to be the set of all integers congruent to \(3\cdot 2^i\pmod{2^{i+2}}\) for any \(i\geq 0\), which has density \(1/2\).
theorem erdos_1136 :
∃ A : Set ℕ, (1 / 3 : ℝ) < A.lowerDensity ∧ AvoidsPowersOfTwo A
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1136.lean, line 53.
Erdos1136.erdos_1136.variants.multiples_of_three
Solved: stated here without proof.
Achieving density \(1/3\) is trivial, taking \(A\) to be all multiples of \(3\).
theorem erdos_1136.variants.multiples_of_three :
AvoidsPowersOfTwo {n : ℕ | 3 ∣ n} ∧ Set.HasDensity {n : ℕ | 3 ∣ n} (1 / 3)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1136.lean, line 61.
Erdos1136.erdos_1136.variants.mueller
Solved: stated here without proof.
Müller [Mu11] settled this question in the affirmative: in fact one can take \(A\) to be the set of all integers congruent to \(3\cdot 2^i\pmod{2^{i+2}}\) for any \(i\geq 0\), which has density \(1/2\).
theorem erdos_1136.variants.mueller :
AvoidsPowersOfTwo muellerSet ∧ muellerSet.HasDensity (1 / 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1136.lean, line 71.
Erdos1136.erdos_1136.variants.upper_bound
Solved: stated here without proof.
Müller also proved this is best possible, in that \(A\) with the property in the question has lower density at most \(1/2\).
theorem erdos_1136.variants.upper_bound (A : Set ℕ) (hA : AvoidsPowersOfTwo A) :
A.lowerDensity ≤ 1 / 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1136.lean, line 80.
Sources
TheoremErdős Problem 1137#
Reference: erdosproblems.com/1137
Quoted from FormalConjectures/ErdosProblems/1137.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/1137.
The file states 1 research or textbook statement: 1 open.
Erdos1137.erdos_1137
Open: stated without proof.
Let \(d_n=p_{n+1}-p_n\), where \(p_n\) denotes the \(n\)th prime. Is it true that
\[\frac{\max_{n < x}d_{n}d_{n-1}}{(\max_{n < x}d_n)^2}\to 0\]as \(x\to \infty\)?
theorem erdos_1137 :
Tendsto (fun x ↦
(((range x).sup (fun n ↦ (primeGap n) * (primeGap (n - 1))) : ℕ) : ℝ) /
(((range x).sup primeGap : ℕ) : ℝ) ^ 2) atTop (𝓝 0)
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1137.lean, line 38.
Sources
TheoremErdős Problem 1138#
References: - erdosproblems.com/1138 - [Va99] Vardi, I., Prime census. (1999). - [Kum26] Kumrawat, S., Disproof of Erdős Problem 1138.
Note that the conjecture has a claimed disproof found at: https://sourish-kumrawat.github.io/papers/Erdos_1138.pdf, see the discussion section on the Erdos problems website for more information.
Quoted from FormalConjectures/ErdosProblems/1138.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/1138.
The file states 1 research or textbook statement: 1 solved.
Erdos1138.erdos_1138
Solved: stated here; a Lean proof is at https://github.com/YanYablonovskiy/formal-conjectures/blob/7c134317104d3b98ecc751afbb79ec0adddf8e7c/FormalConjectures/ErdosProblems/1138a.lean#L496.
Erdős Problem 1138. Let \(x/2 < y < x\) and \(C > 1\). If \(d = \max_{p_n < x}(p_{n+1} - p_n)\), where \(p_n\) denotes the \(n\)-th prime, then is it true that
\[\pi(y + Cd) - \pi(y) \sim \frac{Cd}{\log y}\]?
theorem erdos_1138 : ¬ ∀C > 1,
primeCount_Ioc_mul_const C ~[snd_gt_half_fst] fun (x, y) ↦
C * (sup_primeGap x) / Real.log y
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1138.lean, line 65.
Sources
TheoremErdős Problem 1139#
Reference: erdosproblems.com/1139
Quoted from FormalConjectures/ErdosProblems/1139.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/1139.
The file states 1 research or textbook statement: 1 open.
Erdos1139.erdos_1139
Open: stated without proof.
Let \(1\leq u_1 < u_2 < \cdots\) be the sequence of integers with at most \(2\) prime factors. Is it true that
\[\limsup_{k \to \infty} \frac{u_{k+1}-u_k}{\log k}=\infty?\]
theorem erdos_1139 :
letI u := Nat.nth (fun n ↦ 0 < n ∧ Ω n ≤ 2)
atTop.limsup (fun k : ℕ ↦ (((u (k + 1) : ℝ) - (u k : ℝ)) / Real.log (↑k + 1) : EReal)) = ⊤
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1139.lean, line 38.
Sources
TheoremErdős Problem 1140#
References: - erdosproblems.com/1140 - [EpGi10] Epure, M. and Gica, A., Principal quadratic real fields in connection with some additive problems. Bull. Math. Soc. Sci. Math. Roumanie (N.S.) (2010), 251-259. - [MoWi89] Mollin, R. A. and Williams, H. C., Period four and real quadratic fields of class number one. Proc. Japan Acad. Ser. A Math. Sci. (1989), 89-93. - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
Quoted from FormalConjectures/ErdosProblems/1140.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/1140.
The file states 2 research or textbook statements: 2 solved. It also has 2 test statements, counted here but not shown.
Erdos1140.erdos_1140
Solved: stated here without proof.
Do there exist infinitely many \(n\) such that \(n-2x^2\) is prime for all \(x\) with \(2x^2\lt n\)?
The answer is no: see
erdos_1140.variants.at_most_one_exception.
theorem erdos_1140 : ¬ {n : ℕ | Erdos1140Prop n}.Infinite
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1140.lean, line 67.
Erdos1140.erdos_1140.variants.at_most_one_exception
Solved: stated here without proof.
The known such \(n\) are \(2,5,7,13,31,61,181,199\). It is known that these are, with at most one exception, all such \(n\). An even such \(n\) must be prime (take \(x = 0\)), so \(n = 2\). Theorem 4.1 of Epure and Gica [EpGi10] implies that the only such \(n\equiv 1\pmod{4}\) are \(5,13,61,181\), and their method, coupled with a result of Mollin and Williams [MoWi89], implies that the only such \(n\equiv 3\pmod{4}\) are \(7,31,199\), and at most one other exception.
theorem erdos_1140.variants.at_most_one_exception :
({n : ℕ | Erdos1140Prop n} \ {2, 5, 7, 13, 31, 61, 181, 199}).Subsingleton
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1140.lean, line 79.
Sources
TheoremErdős Problem 1141#
References: - erdosproblems.com/1141 - A214583 - [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). - [Or26] Y. Oriike, Lean formalisation of Erdős problem 1141 (2026) - [Po17] P. Pollack, Bounds for the first several prime character nonresidues. Proc. Amer. Math. Soc. (2017), 2815--2826. - [Me1874] F. Mertens, Ein Beitrag zur analytischen Zahlentheorie. J. Reine Angew. Math. (1874), 46--62. - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
Quoted from FormalConjectures/ErdosProblems/1141.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/1141.
The file states 3 research or textbook statements: 3 solved.
Erdos1141.erdos_1141.variants.pollack_1_3
Solved: stated here without proof.
Theorem 1.3 of [Po17]: for a quadratic character to a large enough modulus, the primes below \(m^{1/4+\varepsilon}\) on which the character is \(1\) outnumber any fixed power of \(\log m\).
theorem erdos_1141.variants.pollack_1_3 (ε A : ℝ) (hε : 0 < ε) (hA : 0 < A) :
∃ m₀ : ℕ, ∀ m : ℕ, m₀ < m → ∀ χ : DirichletCharacter ℂ m, MulChar.IsQuadratic χ →
Real.log m ^ A ≤ ((residuePrimesUpTo m χ ε).card : ℝ)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1141.lean, line 68.
Erdos1141.erdos_1141.variants.mertens_third
Solved: stated here without proof.
Mertens' third theorem [Me1874], in the weakened form the linked proof assumes: the product over the primes up to \(n\) of \(1 - 1/p\) is at least \(1/(3\log n)\).
The true asymptotic is \(e^{-\gamma}/\log n\), and \(e^{-\gamma} > 1/3\), so this bound is weaker than the theorem and is what the deduction needs.
theorem erdos_1141.variants.mertens_third (n : ℕ) (hn : 3 ≤ n) :
1 / (3 * Real.log n) ≤ ∏ p ∈ (Finset.range (n + 1)).filter Nat.Prime, (1 - 1 / (p : ℝ))
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1141.lean, line 81.
Erdos1141.erdos_1141
Solved: stated here; a Lean proof is at https://github.com/Jayyhk/erdos-lean/blob/main/problems/1141/Erdos1141.lean.
Are there infinitely many \(n\) such that \(n-k^2\) is prime for all \(k\) with \((n,k)=1\) and \(k^2 < n\)?
In [Va99] it is asked whether \(968\) is the largest integer with this property, but this is an error, since for example \(968-9=7\cdot 137\).
The list of \(n\) satisfying the given property is [A214583] in the OEIS. The largest known such \(n\) is \(1722\).
The answer is negative: [APSSV26b] proves a stronger finiteness theorem, deducing it from Pollack [Po17]. Oriike [Or26] formalised the deduction in Lean.
theorem erdos_1141 :
¬ Infinite { n | Erdos1141Prop n }
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1141.lean, line 114.
Sources
TheoremErdős Problem 1142#
References: - erdosproblems.com/1142 - A039669 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [MiWe69] Mientka, W. E. and Weitzenkamp, R. C., On f-plentiful numbers, Journal of Combinatorial Theory, Volume 7, Issue 4, December 1969, pages 374-377.
Quoted from FormalConjectures/ErdosProblems/1142.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/1142.
The file states 2 research or textbook statements: 1 open and 1 solved. It also has 8 test statements, counted here but not shown.
Erdos1142.erdos_1142
Open: stated without proof.
Are there infinitely many \(n > 2\) such that \(n - 2^k\) is prime for all \(k \geq 1\) with \(2^k < n\)?
The only known such \(n\) are \(4, 7, 15, 21, 45, 75, 105\) (OEIS A039669).
theorem erdos_1142 :
Infinite { n | Erdos1142Prop n }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1142.lean, line 55.
Erdos1142.erdos_1142.variants.mientka_weitzenkamp
Solved: stated here without proof.
Mientka and Weitzenkamp [MiWe69] proved that the only \(n \leq 2^{44}\) such that \(n > 2\) and \(n - 2^k\) is prime for all \(k \geq 1\) with \(2^k < n\) are \(4, 7, 15, 21, 45, 75, 105\).
theorem erdos_1142.variants.mientka_weitzenkamp :
{ n : ℕ | n ≤ 2 ^ 44 ∧ Erdos1142Prop n } = {4, 7, 15, 21, 45, 75, 105}
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1142.lean, line 64.
Sources
TheoremErdős Problem 1145#
References: - erdosproblems.com/28 - erdosproblems.com/1145
Quoted from FormalConjectures/ErdosProblems/1145.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/1145.
The file states 1 research or textbook statement: 1 open. It also has 1 test statement, counted here but not shown.
Erdos1145.erdos_1145
Open: stated without proof.
Let \(A=\{1\leq a_1 < a_2 < \cdots\}\) and \(B=\{1\leq b_1 < b_2 < \cdots\}\) be sets of integers with \(a_n/b_n\to 1\).
If \(A+B\) contains all sufficiently large positive integers then is it true that \(\limsup 1_A\ast 1_B(n)=\infty\)?
A conjecture of Erdős and Sárközy.
theorem erdos_1145 : Erdos1145Prop
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1145.lean, line 65.
Sources
TheoremErdős Problem 1146#
References: - erdosproblems.com/1146 - [Ru99] Ruzsa, I., Erdős and the Integers. Journal of Number Theory (1999), 115-163.
Quoted from FormalConjectures/ErdosProblems/1146.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/1146.
The file states 1 research or textbook statement: 1 open.
Erdos1146.erdos_1146
Open: stated without proof.
Is \(B=\{2^m3^n : m,n\geq 0\}\) an essential component?
In [Ru99] Ruzsa states "The simplest set with a chance to be an essential component is the collection of numbers in the form \(2^m3^n\) and Erdős often asked whether it is an essential component or not; I do not even have a plausible guess."
theorem erdos_1146 :
IsEssentialComponent { k | ∃ m n : ℕ, k = 2 ^ m * 3 ^ n }
Category research open; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1146.lean, line 54.
Sources
TheoremErdős Problem 1147#
References: - erdosproblems.com/1147 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). - [Ko16b] Konieczny, Jakub, Sets of recurrence as bases for the positive integers. Acta Arith. (2016), 309-338.
Quoted from FormalConjectures/ErdosProblems/1147.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/1147.
The file states 3 research or textbook statements: 3 solved.
Erdos1147.erdos_1147
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1147.lean#L538.
Let \(\alpha>0\) be an irrational number. Is the set
\[A=\left\{ n\geq 1: \| \alpha n^2\| < \frac{1}{\log n}\right\},\]where \(\|\cdot\|\) denotes the distance to the nearest integer, an additive basis of order \(2\)?
This was disproved by Konieczny [Ko16b], and is false both for almost every \(\alpha>0\), and also is false specifically for \(\alpha=\sqrt{2}\).
More generally, given any \(\epsilon(n)\to 0\), the set \(A=\{ n\geq 1: \| \alpha n^2\| < \epsilon(n)\}\) is not an additive basis of order \(2\) for almost every \(\alpha>0\).
theorem erdos_1147 : ¬ ∀ α : ℝ, 0 < α → Irrational α →
(recurrenceSet α fun n ↦ 1 / Real.log n).IsAsymptoticAddBasisOfOrder 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1147.lean, line 56.
Erdos1147.erdos_1147.variants.sqrt_two
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1147.lean#L531.
Konieczny [Ko16b] showed that the set is not an additive basis of order \(2\) for \(\alpha=\sqrt{2}\).
theorem erdos_1147.variants.sqrt_two :
¬ (recurrenceSet (√2) fun n ↦ 1 / Real.log n).IsAsymptoticAddBasisOfOrder 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1147.lean, line 65.
Erdos1147.erdos_1147.variants.almost_every
Solved: stated here without proof.
Konieczny [Ko16b] showed that, given any \(\epsilon(n)\to 0\), the set \(\{ n\geq 1: \| \alpha n^2\| < \epsilon(n)\}\) is not an additive basis of order \(2\) for almost every \(\alpha>0\).
theorem erdos_1147.variants.almost_every : ∀ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) →
∀ᵐ α : ℝ, 0 < α → ¬ (recurrenceSet α ε).IsAsymptoticAddBasisOfOrder 2
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1147.lean, line 75.
Sources
TheoremErdős Problem 1148#
References: - erdosproblems.com/1148 - [Ch26] P. Chojecki, Bounded Representations by \(x^2 + y^2 - z^2\) (2026) - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
Quoted from FormalConjectures/ErdosProblems/1148.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/1148.
The file states 3 research or textbook statements: 2 solved and 1 textbook result.
Erdos1148.erdos_1148
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1148.lean#L238.
Can every large integer \(n\) be written as \(n=x^2+y^2-z^2\) with \(\max(x^2,y^2,z^2)\leq n\)?
This was proved affirmatively by Chojecki [Ch26], using a Duke-type equidistribution theorem. A Lean formalisation of the reduction (conditional on a Duke-type equidistribution theorem) exists; see the forum discussion. The linked formal proof (plby/lean-proofs) removes the Duke hypothesis; it is stated over
ℤ, as∃ N, ∀ n ≥ N, ∃ x y z : ℤ, n = x ^ 2 + y ^ 2 - z ^ 2 ∧ max (x ^ 2) (max (y ^ 2) (z ^ 2)) ≤ n, which gives the statement below by taking absolute values.
theorem erdos_1148 : ∀ᶠ n in atTop, Erdos1148Prop n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1148.lean, line 56.
Erdos1148.erdos_1148.variants.lower_bound
Textbook result, proved here.
The integer \(6563\) cannot be written as \(x^2 + y^2 - z^2\) with \(\max(x^2, y^2, z^2) \leq 6563\).
theorem erdos_1148.variants.lower_bound : ¬ Erdos1148Prop 6563
Category textbook; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1148.lean, line 79.
Erdos1148.erdos_1148.variants.weaker
Solved: stated here without proof.
[Va99] reports this is 'obvious' if we replace \(\leq n\) with \(\leq n+2\sqrt{n}\).
theorem erdos_1148.variants.weaker : ∀ n, erdos_1148_weaker_prop n
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1148.lean, line 95.
Sources
TheoremErdős Problem 1149#
References: - erdosproblems.com/1149 - [BeRi17] Bergelson, Vitaly and Richter, Florian Karl, On the density of coprime tuples of the form \((n,\lfloor f_1(n)\rfloor,\dots,\lfloor f_k(n)\rfloor)\), where \(f_1,\dots,f_k\) are functions from a Hardy field. Number Theory - Diophantine Problems, Uniform Distribution and Applications, Springer (2017), 109-135. arXiv:1611.08044 - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
Quoted from FormalConjectures/ErdosProblems/1149.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/1149.
The file states 1 research or textbook statement: 1 solved.
Erdos1149.erdos_1149
Solved: stated here; a Lean proof is at https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/latest/ErdosProblems/Erdos1149.lean#L136.
Let \(\alpha>0\) be a real number, not an integer. The density of integers \(n\geq 1\) for which \((n,\lfloor n^\alpha\rfloor)=1\) is \(6/\pi^2\).
This is true, and was proved by Bergelson and Richter [BeRi17].
theorem erdos_1149 (α : ℝ) (hα : 0 < α) (hα' : α ∉ Set.range ((↑) : ℤ → ℝ)) :
{n : ℕ | 1 ≤ n ∧ n.Coprime ⌊(n : ℝ) ^ α⌋₊}.HasDensity (6 / Real.pi ^ 2)
Category research solved; AMS 11 Number theory. Declared in FormalConjectures/ErdosProblems/1149.lean, line 46.
Sources
TheoremErdős Problem 1150#
References: - erdosproblems.com/1150 - [OAI26a] OpenAI, Asymptotically minimal maxima of real Littlewood polynomials. OpenAI Math Release preprint (2026). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Asymptotically-minimal-maxima-of-real-Littlewood-polynomials-September-23-2026/paper.pdf
Quoted from FormalConjectures/ErdosProblems/1150.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/1150.
The file states 2 research or textbook statements: 1 solved and 1 textbook result.
Erdos1150.erdos_1150
Solved: stated here; a Lean proof is at https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/Littlewood/Main.lean#L187.
Is there some constant \(c > 0\) such that, for all large enough \(n\) and all polynomials \(P\) of degree \(n\) with coefficients in \(\{-1, 1\}\),
\[\max_{|z|=1} |P(z)| > (1 + c) \sqrt{n}?\]No. This was disproved by an internal OpenAI model in September 2026 [OAI26a]; see the linked Lean proof.
theorem erdos_1150 :
¬ ∃ c > 0, ∀ᶠ n in Filter.atTop,
∀ P : ℂ[X], (∀ i ≤ P.natDegree, P.coeff i = - 1 ∨ P.coeff i = 1) → P.natDegree = n →
⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ > (1 + c) * Real.sqrt n
Category research solved; AMS 12 Field theory and polynomials, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1150.lean, line 47.
Erdos1150.erdos_1150.variants.parseval_lower_bound
Textbook result, proved here.
The trivial lower bound from Parseval's identity: for any polynomial \(P\) of degree \(n\) with coefficients in \(\{-1, 1\}\), we have \(\max_{|z|=1} |P(z)| \geq \sqrt{n+1}\).
This follows from Parseval's identity:
\[\frac{1}{2\pi} \int_0^{2\pi} |P(e^{i\theta})|^2 d\theta = \sum_{k=0}^{n} |a_k|^2 = n+1\]since each \(|a_k|^2 = 1\). The circle average is bounded by the pointwise supremum squared, so \(\max_{|z|=1} |P(z)|^2 \ge n+1\), whence \(\max_{|z|=1} |P(z)| \ge \sqrt{n+1}\).
theorem erdos_1150.variants.parseval_lower_bound (P : ℂ[X]) (n : ℕ)
(hcoeff : ∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1)
(hdeg : P.natDegree = n) :
⨆ z : Metric.sphere (0 : ℂ) 1, ‖P.eval (z : ℂ)‖ ≥ Real.sqrt (n + 1)
Category textbook; AMS 12 Field theory and polynomials, 30 Functions of a complex variable. Declared in FormalConjectures/ErdosProblems/1150.lean, line 63.
Sources
TheoremErdős Problem 1152#
References: - erdosproblems.com/1152 - [EKS89] Erdős, P., Kroó, A. and Szabados, J., On convergent interpolatory polynomials. J. Approx. Theory 58 (1989), 232-241. PDF - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999).
Quoted from FormalConjectures/ErdosProblems/1152.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/1152.
The file states 1 research or textbook statement: 1 open.
Erdos1152.erdos_1152
Open: stated without proof.
For \(n\geq 1\) fix some sequence of \(n\) distinct numbers \(x_{1n},\ldots,x_{nn}\in [-1,1]\). Let \(\epsilon=\epsilon(n)\to 0\).
Does there always exist a continuous function \(f:[-1,1]\to \mathbb{R}\) such that if \(p_n\) is a sequence of polynomials, with degrees \(\deg p_n<(1+\epsilon(n))n\), such that \(p_n(x_{kn})=f(x_{kn})\) for all \(1\leq k\leq n\), then \(p_n(x)\not\to f(x)\) for almost all \(x\in [-1,1]\)?
This is Problem 2.42 in [Va99]. The \(n\) nodes of the \(n\)-th row form the finite set
nodes n. We take \(\epsilon(n)>0\). A smaller \(\epsilon\) only shrinks the class of \(p_n\), so this is equivalent to allowing any real \(\epsilon(n)\to 0\). We impose the degree bound only for \(n\geq 1\), since for \(n=0\) the boundnatDegree < 0can never hold. We read "\(p_n(x)\not\to f(x)\) for almost all \(x\)" as: for almost every \(x\), the sequence \(p_n(x)\) does not converge to \(f(x)\).For \(\deg p_n\lt n\) the interpolating polynomial is unique (the Lagrange polynomial). Erdős, Kroó and Szabados [EKS89, pp. 232-233] give necessary and sufficient conditions on the nodes under which, for every continuous \(f\) and every fixed \(\epsilon>0\), there are interpolating polynomials of degree at most \(\lfloor n(1+\epsilon)\rfloor\) approximating \(f\) at the rate of the best uniform approximation (in particular converging uniformly to \(f\)).
theorem erdos_1152 :
∀ nodes : ℕ → Finset ℝ, (∀ n, (nodes n).card = n) →
(∀ n, ∀ x ∈ nodes n, x ∈ Set.Icc (-1 : ℝ) 1) →
∀ ε : ℕ → ℝ, (∀ n, 0 < ε n) → Tendsto ε atTop (𝓝 0) →
∃ f : ℝ → ℝ, ContinuousOn f (Set.Icc (-1 : ℝ) 1) ∧
∀ p : ℕ → ℝ[X],
(∀ n : ℕ, 1 ≤ n → ((p n).natDegree : ℝ) < (1 + ε n) * n) →
(∀ n, ∀ x ∈ nodes n, (p n).eval x = f x) →
∀ᵐ t ∂(volume.restrict (Set.Icc (-1 : ℝ) 1)),
¬ Tendsto (fun n => (p n).eval t) atTop (𝓝 (f t))
Category research open; AMS 41 Approximations and expansions. Declared in FormalConjectures/ErdosProblems/1152.lean, line 61.
Sources
TheoremErdős Problem 1154#
References: - erdosproblems.com/1154 - [ErVo66] Erdős, Paul and Volkmann, Bodo, Additive Gruppen mit vorgegebener Hausdorffscher Dimension. J. Reine Angew. Math. (1966), 203--208. - [EdMi01] Edgar, G. A. and Miller, Chris, Hausdorff dimension, analytic sets and transcendence. Real Anal. Exchange (2001/02), 335--339. - [EdMi03] Edgar, G. A. and Miller, Chris, Borel subrings of the reals. Proc. Amer. Math. Soc. (2003), 1121--1129. - [Ma16b] Mauldin, R. Daniel, Subfields of ℝ with arbitrary Hausdorff dimension. Math. Proc. Cambridge Philos. Soc. (2016), 157--165.
Quoted from FormalConjectures/ErdosProblems/1154.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/1154.
The file states 5 research or textbook statements: 2 open and 3 solved. It also has 2 test statements, counted here but not shown.
Erdos1154.erdos_1154.parts.i
Open: stated without proof.
Does there exist, for every \(\alpha \in [0, 1]\), a ring in \(\mathbb{R}\) with Hausdorff dimension \(\alpha\)?
theorem erdos_1154.parts.i :
∀ a ∈ Icc (0 : ℝ≥0∞) 1, ∃ R : Subring ℝ, dimH (R : Set ℝ) = a
Category research open; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1154.lean, line 49.
Erdos1154.erdos_1154.parts.ii
Open: stated without proof.
Does there exist, for every \(\alpha \in [0, 1]\), a field in \(\mathbb{R}\) with Hausdorff dimension \(\alpha\)?
theorem erdos_1154.parts.ii :
∀ a ∈ Icc (0 : ℝ≥0∞) 1, ∃ R : Subfield ℝ, dimH (R : Set ℝ) = a
Category research open; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1154.lean, line 58.
Erdos1154.erdos_1154.variants.group
Solved: stated here without proof.
For every \(\alpha \in [0, 1]\), there exists an additive group in \(\mathbb{R}\) with Hausdorff dimension \(\alpha\). This is proved in [ErVo66].
theorem erdos_1154.variants.group {a : ℝ≥0∞} (ha : a ∈ Icc 0 1) :
∃ R : AddSubgroup ℝ, dimH (R : Set ℝ) = a
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1154.lean, line 67.
Erdos1154.erdos_1154.variants.analytic_ring
Solved: stated here without proof.
If a subring is analytic, then it is either equal to \(\mathbb{R}\) or its Hausdorff dimension is equal to \(0\). This is proved in [EdMi03], superseding the earlier result of [EdMi01] that a real closed analytic subfield of \(\mathbb{R}\) has Hausdorff dimension \(0\) or \(1\).
theorem erdos_1154.variants.analytic_ring {R : Subring ℝ} (hR : AnalyticSet (R : Set ℝ)) :
R = ⊤ ∨ dimH (R : Set ℝ) = 0
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1154.lean, line 77.
Erdos1154.erdos_1154.variants.continuumHypothesis_field
Solved: stated here without proof.
Assume the continuum hypothesis, then for every \(\alpha \in [0, 1]\), there exists a field in \(\mathbb{R}\) with Hausdorff dimension \(\alpha\). This is proved in [Ma16b].
theorem erdos_1154.variants.continuumHypothesis_field {a : ℝ≥0∞} (ha : a ∈ Icc 0 1)
[Fact (ℵ₁ = 𝔠)] :
∃ R : Subfield ℝ, dimH (R : Set ℝ) = a
Category research solved; AMS 28 Measure and integration. Declared in FormalConjectures/ErdosProblems/1154.lean, line 86.
Sources
TheoremErdős Problem 1157#
References: - erdosproblems.com/1157 - [BES73] Brown, W. G. and Erdős, P. and S\'os, V. T., Some extremal problems on {\(r\)}-graphs. (1973), 53--63.
Quoted from FormalConjectures/ErdosProblems/1157.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/1157.
The file states 1 research or textbook statement: 1 open.
Erdos1157.erdos_1157
Open: stated without proof.
Let \(s,k,r\geq 2\). Let \(\mathcal{F}\) be the family of all \(r\)-uniform hypergraphs with \(k\) vertices and \(s\) edges. Determine
\[\mathrm{ex}_r(n,\mathcal{F}).\]
theorem erdos_1157 :
∀ r k s : ℕ, 2 ≤ r → 2 ≤ k → 2 ≤ s → ∀ n : ℕ,
Hypergraph.configurationExtremalNumber n r k s = erdos_1157.answer n r k s
Category research open; AMS 05 Combinatorics. Declared in FormalConjectures/ErdosProblems/1157.lean, line 43.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.