Vela Mathematics Program: problems

Problem ledger

1,217 problems · 11/25Number SourcesGraph view

declared open · formalizederdos:501

x \in \mathbb{R}

let

A_x \subset \mathbb{R}

be a bounded set of Lebesgue outer measure

< 1

. Must there be an infinite independent set, that is an infinite

X \subseteq \mathbb{R}

with

x \notin A_y

for all distinct

x, y \in X

? Erdős and Hajnal proved that arbitrarily large finite independent sets exist. Hechler showed in 1972 that the answer is no under the continuum hypothesis, so any positive answer had to come from a model where CH fails, and Sungchul Lee later derived one from a real-valued measurable cardinal. The answer is that neither side is provable. Dropping Lee's large cardinal by transferring his argument to the extension of a model of CH by random reals gives a model where the answer is yes; Hechler's construction gives one where it is no. The question is independent of ZFC.

combinatoricsset theoryN/A4 sources

declared solved (Lean) · formalizederdos:502

∀ (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))), A.Finite → {d | ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ dist x y = d}.ncard = 2 → A.ncard ≤ (n + 2).choose 2

geometrydistancesA0276275 sources

declared open · formalizederdos:503

∀ (n : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A.IsIsosceles), A.ncard = x} sorry

geometrydistancesA1757693 sources

declared solvederdos:504

Erdős problem 504

geometryN/A

declared disproved (Lean) · formalizederdos:505

∃ n S, Bornology.IsBounded S ∧ 0 < Metric.diam S ∧ ∀ (F : Fin (n + 1) → Set (EuclideanSpace ℝ (Fin n))), S ⊆ ⋃ i, F i → ∃ i, Metric.diam S ≤ Metric.diam (F i)

geometrypossible5 sources

declared decidableerdos:506

Erdős problem 506

geometrypossible

declared open · formalizederdos:507

Asymptotics.IsEquivalent Filter.atTop Erdos507.α sorry

geometryN/A3 sources

declared open · formalizederdos:508

4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber

geometryramsey theoryN/A2 sources

declared open · formalizederdos:509

∀ {M : Type u} [inst : MetricSpace M] (S : Set M), S.Nonempty → ∀ (r : ℝ) (ι : Type v) (bdc : Erdos509.BoundedDiscCover S r ι), 0 < r

analysisN/A2 sources

declared open · formalizederdos:510

sorry ↔ ∃ c, ∃ (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ θ, ∑ n ∈ A, Real.cos (↑n * θ) < -c * √↑N

analysisN/A2 sources

declared disprovederdos:511

Erdős problem 511

analysisN/A

declared proved (Lean) · formalizederdos:512

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

analysisN/A4 sources

declared open · formalizederdos:513

sorry = ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop

analysisN/A3 sources

declared openerdos:514

For a transcendental entire function, how fast can

|f(z)|

be forced to grow along a path to infinity, and how short can such a path be in terms of the maximum modulus

M(r, f)

analysisN/A4 sources

declared provederdos:515

Erdős problem 515

analysisN/A

declared proved · formalizederdos:516

∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (n : ℕ), a n ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → Erdos516.OfFiniteOrder f → Filter.limsup (fun r => Erdos516.ratio r f) Filter.atTop = 1

analysisN/A2 sources

declared open · formalizederdos:517

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

analysisN/A3 sources

declared provederdos:518

Erdős problem 518

graph theoryramsey theoryN/A

declared proved (Lean) · formalizederdos:519

True ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ k, c < ‖Erdos519.powerSum z (↑k + 1)‖

analysisN/A5 sources

declared open · formalizederdos:520

True ↔ ∃ c > 0, ∀ (Ω : Type) [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] (f : ℕ → Ω → ℝ), Erdos520.IsRademacherMultiplicative f → ∀ᵐ (ω : Ω), Filter.limsup (fun N => ∑ m ∈ Finset.Iic N, f m ω / √(↑N * Real.log (Real.log ↑N))) Filter.atTop = c

number theoryprobabilityN/A2 sources

declared open · formalizederdos:521

False ↔ Erdos521.Claim

analysispolynomialsprobabilityN/A4 sources

declared open · formalizederdos:522

For

P_n(z) = \sum_{k=0}^n \varepsilon_k z^k

with independent uniform signs, does the number

R_n

of roots in

|z| \le 1

satisfy

R_n/(n/2) \to 1

almost surely? The manuscript proves the strong law with

R_n = n/2 + O_\omega(n^{149/150})

analysispolynomialsprobabilityN/A4 sources

declared provederdos:523

Erdős problem 523

analysisprobabilitypolynomialsN/A

declared openerdos:524

Erdős problem 524

analysisprobabilitypolynomialsN/A3 sources

declared provederdos:525

Erdős problem 525

analysisprobabilitypolynomialspossible

declared solvederdos:526

Erdős problem 526

probabilitygeometryN/A

declared provederdos:527

Erdős problem 527

analysisprobabilityN/A

declared openerdos:528

Erdős problem 528

geometryA387897 · A156816

declared openerdos:529

Erdős problem 529

geometryprobabilityN/A

declared openerdos:530

Erdős problem 530

number theorysidon setsA143824 · possible

declared openerdos:531

Erdős problem 531

number theoryramsey theorypossible

declared proved (Lean) · formalizederdos:532

True ↔ ∀ (c : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∃ color, ∀ (S : Finset ℕ), S.Nonempty → ↑S ⊆ A → c (∑ n ∈ S, n) = color

number theoryramsey theoryN/A4 sources

declared disproved · formalizederdos:533

False ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 5 → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ∃ S, c * ↑n ≤ ↑S.card ∧ G.CliqueFreeOn (↑S) 3

graph theoryN/A3 sources

declared solvederdos:534

Erdős problem 534

number theoryintersecting familyA387543 · A387698

declared open · formalizederdos:535

∀ r ≥ 3, ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos535.f r N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))

number theorypossible3 sources

declared open · formalizederdos:536

True ↔ ∀ ε > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ε * ↑N ≤ ↑A.card → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, {a, b, c}.card = 3 ∧ a.lcm b = b.lcm c ∧ b.lcm c = a.lcm c

number theorypossible3 sources

declared disproved (Lean) · formalizederdos:537

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ ε * ↑N → ∃ a₁ ∈ A, ∃ a₂ ∈ A, ∃ a₃ ∈ A, ∃ p₁ p₂ p₃, Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ p₁ ≠ p₂ ∧ p₁ ≠ p₃ ∧ p₂ ≠ p₃ ∧ a₁ * p₁ = a₂ * p₂ ∧ a₂ * p₂ = a₃ * p₃

number theorypossible5 sources

declared open · formalizederdos:538

If each integer has at most

r

representations

m = pa

with

p

prime and

a \in A \subseteq [1, N]

, what is the best upper bound for

\sum_{a \in A} 1/a

? The candidate proof gives the matching order

\Theta_r(\log N / \log\log N)

number theoryN/A5 sources

declared open · formalizederdos:539

For

|A| = n

, how small can the cofactor set

Q(A) = \{a / \gcd(a,b) : a, b \in A\}

be? The answer is

h(n) = n^{1/2 + o(1)}

: a new upper bound

h(n) \le n^{1/2} \exp(O(\sqrt{\log n}))

matches the classical lower bound.

number theorypossible5 sources

declared proved (Lean) · formalizederdos:540

True ↔ ∃ C, 0 < C ∧ ∀ (N : ℕ), 0 < N → ∀ (A : Finset (ZMod N)), C * √↑N ≤ ↑A.card → Erdos540.HasZeroSubsetSum A

number theoryA0344635 sources

declared proved (Lean) · formalizederdos:541

True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (a : Fin p → ZMod p), (∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2

number theoryN/A5 sources

declared solvederdos:542

Erdős problem 542

number theoryN/A

declared disprovederdos:543

Erdős problem 543

number theorygroup theorypossible3 sources

declared openerdos:544

Erdős problem 544

graph theoryramsey theoryA000791

declared openerdos:545

Erdős problem 545

graph theoryramsey theoryA059442 · possible

declared provederdos:546

Erdős problem 546

graph theoryramsey theorypossible

declared decidableerdos:547

Erdős problem 547

graph theoryramsey theoryN/A

declared falsifiableerdos:548

Erdős problem 548

graph theoryN/A

declared disprovederdos:549

Erdős problem 549

graph theoryramsey theoryN/A

declared openerdos:550

Let

m_1\leq\cdots\leq m_k

and

n

be sufficiently large. If

T

is a tree on

n

vertices and

G

is the complete multipartite graph with vertex class sizes

m_1,\ldots,m_k

, prove that

R(T,G)\leq (\chi(G)-1)(R(T,K_{m_1,m_2})-1)+m_1

graph theoryramsey theoryN/A4 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science