Vela Mathematics Program: problems

Problem ledger

1,217 problems · 3/25Number SourcesGraph view

declared open · formalized · $100erdos:101

(fun n => ↑(Erdos101.numLinesWithFourPointMax n)) =o[Filter.atTop] fun n => ↑n ^ 2

geometryA006065 · possible2 sources

declared openerdos:102

Erdős problem 102

geometryN/A

declared openerdos:103

Erdős problem 103

geometrydistancespossible

declared open · $100erdos:104

Erdős problem 104

geometryA003829

declared disproved (Lean) · formalized · $50erdos:105

False ↔ ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Disjoint A B → A.card = B.card + 3 → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}

geometryN/A5 sources

declared falsifiableerdos:106

f(n)

is the maximum total side length of

n

interior-disjoint squares packed in the unit square, is

f(k^2 + 1) = k

? An exact rational configuration packs

17

squares with total side length greater than

4

, refuting the identity at

k = 4

geometryN/A3 sources

declared falsifiable · formalized · $500erdos:107

sorry ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1

geometryconvexA0000512 sources

declared open · formalizederdos:108

True ↔ ∀ r ≥ 4, ∀ k ≥ 2, ∃ f, ∀ (V : Type u) (G : SimpleGraph V), Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k

graph theorychromatic numbercyclespossible2 sources

declared proved · formalizederdos:109

∀ (A : Set ℕ), A.upperDensity > 0 → ∃ B C, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

additive combinatoricsN/A2 sources

declared disprovederdos:110

Erdős problem 110

graph theorychromatic numbercyclesN/A

declared openerdos:111

Erdős problem 111

graph theorychromatic numberset theoryN/A

declared openerdos:112

Erdős problem 112

graph theoryramsey theorypossible

declared disproved · $500erdos:113

Erdős problem 113

graph theoryturan numberN/A

declared falsifiable · $250erdos:114

Erdős problem 114

polynomialsanalysisN/A

declared proved (Lean) · formalizederdos:115

True ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : Polynomial ℂ), p.Monic → p.natDegree = n → IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} → ∀ (z : ℂ), ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2

polynomialsanalysisN/A5 sources

declared provederdos:116

Erdős problem 116

polynomialsanalysisN/A

declared openerdos:117

Erdős problem 117

group theorypossible

declared disprovederdos:118

Erdős problem 118

set theoryramsey theoryN/A

declared solved · formalized · $100erdos:119

For unit-modulus complex numbers

z_i

, let

p_n(z)=\prod_{i\le n}(z-z_i)

and

M_n=\max_{|z|=1}|p_n(z)|

. Erdős's prize question: is there

c>0

with

\sum_{k\le n} M_k > n^{1+c}

analysispolynomialsN/A4 sources

declared open · formalized · $100erdos:120

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

combinatoricsN/A3 sources

declared disprovederdos:121

Erdős problem 121

number theorysquaresA028391 · A013928 · A372306 · A373319 · A372306 · A373178 · A360659 · A373114 · A143301

declared openerdos:122

Erdős problem 122

number theoryN/A

declared proved (Lean) · formalized · $250erdos:123

Let

a,b,c>1

be pairwise coprime integers. Is every large integer a sum of distinct numbers of the form

a^k b^l c^m

(

k,l,m\ge 0

), none dividing another?

number theoryN/A5 sources

declared open · formalizederdos:124

∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹

number theorybase representationsN/A4 sources

declared disproved (Lean) · formalizederdos:125

False ↔ ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity

number theorybase representationsA3670906 sources

declared open · formalized · $250erdos:126

True ↔ ∀ (f : ℕ → ℕ), Erdos126.IsMaximalAddFactorsCard f → Filter.Tendsto (fun n => ↑(f n) / Real.log ↑n) Filter.atTop Filter.atTop

number theorypossible2 sources

declared provederdos:127

Erdős problem 127

graph theorypossible

declared falsifiable · formalized · $250erdos:128

True ↔ ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), (∀ (V' : Set V), 2 * V'.ncard + 1 ≥ Fintype.card V → 50 * (SimpleGraph.induce V' G).edgeSet.ncard > Fintype.card V ^ 2) → ¬G.CliqueFree 3

graph theoryN/A2 sources

declared openerdos:129

Erdős problem 129

graph theoryramsey theorypossible

declared open · formalizederdos:130

For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.

graph theorychromatic numberN/A4 sources

declared openerdos:131

Let

F(N)

be the maximal size of

A\subseteq\{1,\ldots,N\}

such that no

a\in A

divides the sum of any nonempty subset of

A\setminus\{a\}

. Estimate

F(N)

. The lower bound

F(N)\gg N^{1/5}

is classical, from constructions of Erdős and Csaba, and every non-dividing set is non-averaging, which gave

F(N)\leq N^{1/4+o(1)}

. The claimed new result is the matching upper bound

F(N)\leq N^{1/5+o(1)}

, obtained by running the Pham-Zakharov density-increment argument one dimension lower through a projective normalization, hence

F(N)=N^{1/5+o(1)}

number theoryA0680632 sources

declared open · $100erdos:132

Erdős problem 132

distancesN/A

declared disprovederdos:133

Erdős problem 133

graph theorypossible

declared proved (Lean) · formalizederdos:134

True ↔ ∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∃ N, ∀ n ≥ N, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 3 → (∀ (v : Fin n), ↑(G.degree v) < (↑n).rpow (1 / 2 - ε)) → ∃ H, G ≤ H ∧ H.CliqueFree 3 ∧ (∀ (x y : Fin n), x ≠ y → H.Adj x y ∨ ∃ z, H.Adj x z ∧ H.Adj z y) ∧ ↑(H.edgeFinset \ G.edgeFinset).card ≤ δ * ↑n ^ 2

graph theoryN/A5 sources

declared disproved · $250erdos:135

Erdős problem 135

distancesgeometrypossible

declared solvederdos:136

Erdős problem 136

graph theorypossible

declared open · formalizederdos:137

sorry ↔ ∀ k ≥ 3, ∀ (n : ℕ), ¬(∏ x ∈ Finset.Ioc n (n + k), x).Powerful

number theoryN/A2 sources

declared open · formalized · $500erdos:138

W(k)

is the least

N

such that every two-colouring of

\{1, \dots, N\}

contains a monochromatic

k

-term arithmetic progression, must

W(k+1) - W(k) \to \infty

additive combinatoricsA0053464 sources

declared proved · formalized · $1000erdos:139

∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared proved · $500erdos:140

Erdős problem 140

additive combinatoricsarithmetic progressionsA003002

declared open · formalizederdos:141

sorry ↔ ∀ k ≥ 3, ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s k

additive combinatoricsprimesarithmetic progressionsA0065602 sources

declared open · formalized · $10000erdos:142

∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources

declared open · formalized · $500erdos:143

True ↔ ∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Filter.liminf (fun x => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0

primitive setsN/A2 sources

declared proved · $250erdos:144

Erdős problem 144

number theorydivisorsA005279

declared open · formalizederdos:145

True ↔ ∀ α ≥ 0, ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)

number theoryA0051172 sources

declared open (Lean) · formalized · $500erdos:146

H

is bipartite and

r

-degenerate, is

\mathrm{ex}(n;H) \ll n^{2-1/r}

(a $500 Erdős-Simonovits prize conjecture)? A counterexample refutes the degeneracy conjecture.

graph theoryturan numberN/A3 sources

declared disproved · $500erdos:147

Erdős problem 147

graph theoryturan numberN/A

declared openerdos:148

Erdős problem 148

number theoryunit fractionsA076393 · A006585

declared openerdos:149

Erdős problem 149

graph theoryN/A

declared proved (Lean) · formalizederdos:150

True ↔ ∃ α < 2, Filter.Tendsto (fun n => ↑(Erdos150.maxMinimalCuts n) ^ (1 / ↑n)) Filter.atTop (nhds α)

graph theorypossible5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science