Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 11/13Number SourcesGraph view

declared openerdos:1030

graph theoryramsey theoryA000791 · A059442

declared openerdos:1032

Do arbitrarily large 4-chromatic edge-critical graphs exist with minimum degree bounded below by a positive constant times the number of vertices?

graph theorychromatic numberpossible3 sources

declared openerdos:1033

Erdős problem 1033

graph theorypossible2 sources

declared openerdos:1035

Erdős problem 1035

graph theorypossible

declared open · formalizederdos:1038

Among all nonconstant monic polynomials

f

whose roots lie in

[-1, 1]

, determine

\inf_f |\{x \in \mathbb{R} : |f(x)| < 1\}|

analysisN/A4 sources

declared openerdos:1039

For

f(z) = \prod_{i=1}^n (z - z_i)

with all

|z_i| \le 1

, let

\rho(f)

be the radius of the largest disc contained in

\{z : |f(z)| < 1\}

. Is

\rho(f) \gg 1/n

? The worst case is now known to be

\Theta(1/n)

, with the explicit bound

\rho(f) \ge (\log 2)/n

analysisN/A3 sources

declared openerdos:1040

For a closed infinite set

F \subseteq \mathbb{C}

, let

\mu(F)

be the infimum of

|\{z : |f(z)| < 1\}|

over monic polynomials with zeros in

F

. Is

\mu(F)

determined only by the transfinite diameter of

F

analysisN/A3 sources

declared openerdos:1045

Erdős problem 1045

analysisN/A

declared open · formalizederdos:1049

True ↔ ∀ t > 1, Irrational (∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1))

irrationalityN/A2 sources

declared open · formalized · $10erdos:1052

sorry ↔ {n | Erdos1052.IsUnitaryPerfect n}.Finite

number theoryA0028272 sources

declared openerdos:1053

Erdős problem 1053

number theoryA007539

declared open · formalizederdos:1054

sorry ↔ (fun n => ↑(Erdos1054.f n)) =o[Filter.atTop] fun n => ↑n

number theorydivisorsA1674853 sources

declared open · formalizederdos:1055

∀ (r : ℕ+), {p | Nat.Prime p ∧ Erdos1055.IsOfClass r p}.Infinite

number theoryprimesA0051132 sources

declared open · formalizederdos:1056

True ↔ ∀ k ≥ 2, ∃ p, ∃ (_ : Nat.Prime p), ∃ boundaries, ∃ (_ : StrictMono boundaries), Erdos1056.AllModProdEqualsOne p boundaries

number theoryA0604273 sources

declared open · formalizederdos:1057

True ↔ Filter.Tendsto (fun x => Real.log (Erdos1057.carmichaelCounting x) / Real.log x) Filter.atTop (nhds 1)

number theoryA0069312 sources

declared open · formalizederdos:1059

Erdos1059.AllFactorialSubtractionsComposite 101

number theoryprimesA0641522 sources

declared open · formalizederdos:1060

∃ h, (h =o[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card ≤ ↑n ^ h n

number theoryA3271532 sources

declared open · formalizederdos:1061

Let

S(x)

count ordered pairs

(a,b)

with

a+b \le x

and

\sigma(a)+\sigma(b) = \sigma(a+b)

. Erdos asked whether

S(x) \sim cx

. The opposite extreme holds: for every

R > 0

S(x)/(x(\log x)^R) \to \infty

, so the count beats every fixed logarithmic scale.

number theoryA110177 · possible4 sources

declared open · formalizederdos:1062

(∃ l, Filter.Tendsto (fun n => ↑(Erdos1062.f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ True

number theoryA0383723 sources

declared open · formalizederdos:1063

have upper_bound := sorry; (fun k => ↑(Erdos1063.n k)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun k => ↑k * (Finset.Icc 1 (k - 1)).lcm fun n => ↑n

number theoryA3893603 sources

declared open · formalizederdos:1065

True ↔ {p | ∃ q k, Nat.Prime p ∧ Nat.Prime q ∧ p = 2 ^ k * q + 1}.Infinite

number theoryA074781 · A3394652 sources

declared openerdos:1066

Erdős problem 1066

graph theoryplanar graphspossible

declared open · formalizederdos:1068

True ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ s, s.Countable ∧ (SimpleGraph.induce s G).InfinitelyConnected

graph theoryset theorychromatic numberN/A2 sources

declared openerdos:1070

Erdős problem 1070

geometrypossible2 sources

declared open · formalizederdos:1072

True ↔ {p | Nat.Prime p ∧ Erdos1072.f p = p - 1}.Infinite

number theoryA073944 · A072937 · A1545542 sources

declared open · formalizederdos:1073

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ (x : ℕ), Erdos1073.A x ≤ ↑x ^ o x

number theoryA2565192 sources

declared open · formalizederdos:1074

sorry ↔ ∃ c, Erdos1074.EHSNumbers.HasDensity c

number theoryA063980 · A0641642 sources

declared openerdos:1075

Erdős problem 1075

hypergraphsN/A

declared openerdos:1083

Erdős problem 1083

geometrydistancesA186704 · possible

declared open · formalizederdos:1084

∀ {n : ℕ}, n ≠ 0 → Erdos1084.f 2 n < 3 * n

geometrydistancesA045945 · possible3 sources

declared open · formalizederdos:1085

∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (1 + c / Real.log (Real.log ↑n)) < ↑(Erdos1085.f 2 n)

geometrydistancesA186705 · possible2 sources

declared openerdos:1086

Erdős problem 1086

geometrydistancespossible

declared openerdos:1087

Erdős problem 1087

geometrydistancespossible

declared openerdos:1088

Erdős problem 1088

geometrypossible

declared open · formalizederdos:1093

sorry ↔ {x | have k := x.1; have n := x.2; 2 * k ≤ n ∧ Erdos1093.deficiency n k = 1 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ n.choose k → k < p}.Infinite

number theorybinomial coefficientsN/A2 sources

declared open · formalizederdos:1094

{(n, k) | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite

number theorybinomial coefficientsN/A2 sources

declared open · formalizederdos:1095

Asymptotics.IsEquivalent Filter.atTop (fun k => Real.log ↑(Erdos1095.g k)) fun k => ↑k / Real.log ↑k

number theorybinomial coefficientsA0034584 sources

declared open · formalizederdos:1097

False ↔ ∃ C > 0, ∀ (A : Finset ℤ), ↑(Erdos1097.CommonDifferencesThreeTermAP A).ncard ≤ C * ↑A.card ^ (3 / 2)

number theoryadditive combinatoricsN/A3 sources

declared openerdos:1100

Erdős problem 1100

number theorydivisorsA325864 · possible2 sources

declared open · formalizederdos:1101

Does there exist a good pairwise-coprime sequence

u_n

with

\sum 1/u_n < \infty

and polynomial growth? What if one only requires

u_n \le e^{o(n)}

number theoryN/A4 sources

declared openerdos:1103

Erdős problem 1103

number theoryA392164

declared open · formalizederdos:1104

∃ c₁, 0 < c₁ ∧ c₁ ≤ 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, c₁ * √↑n / √(Real.log ↑n) ≤ ↑(Erdos1104.triangleFreeMaxChromatic n)

graph theorychromatic numberA2925282 sources

declared open · formalizederdos:1106

True ↔ Filter.Tendsto (fun n => (∏ i ∈ Finset.Icc 1 n, Erdos1106.p i).primeFactors.card) Filter.atTop Filter.atTop

number theoryA194259 · A1942602 sources

declared open · formalizederdos:1107

∀ r ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1107.SumOfRPowerful r n

number theorypowerfulA056828 · A392342 · A392343 · possible2 sources

declared open · formalizederdos:1108

True ↔ ∀ k ≥ 2, {a | a ∈ Erdos1108.FactorialSums ∧ ∃ m, m ^ k = a}.Finite

number theoryfactorialsA051761 · A115645 · A0254942 sources

declared openerdos:1109

Erdős problem 1109

number theoryA392164 · A392165

declared open · formalizederdos:1110

True ↔ ∀ (p q : ℕ), q < p → 2 ≤ q → p.Coprime q → ¬(p = 3 ∧ q = 2) → {n | n.Coprime (p * q) ∧ ¬Erdos1110.Representable p q n}.Infinite

number theorypossible2 sources

declared openerdos:1111

Erdős problem 1111

graph theorypossible

declared open · formalizederdos:1113

sorry ↔ ∃ k, k.IsSierpinskiNumber ∧ ¬Erdos1113.HasFinitePrimeCoveringSet k

number theorycovering systemsA0763362 sources

declared openerdos:1117

Erdős problem 1117

analysisN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science