Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 9/13Number SourcesGraph view

declared open · formalizederdos:826

True ↔ ∃ C > 0, {n | ∀ k ≥ 1, ↑((ArithmeticFunction.sigma 0) (n + k)) ≤ C * ↑k}.Infinite

number theoryN/A2 sources

declared openerdos:827

Erdős problem 827

geometrypossible

declared open · formalizederdos:828

True ↔ ∀ (a : ℤ), {n | ↑n.totient ∣ ↑n + a}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:829

True ↔ ∃ C, (fun n => ↑(AdditiveCombinatorics.sumRep Erdos829.cubes n)) =O[Filter.atTop] fun n => Real.log ↑n ^ C

number theorypossible2 sources

declared open · formalizederdos:830

sorry ↔ {(a, b) | IsAmicable a b}.Infinite

number theoryA2591802 sources

declared openerdos:831

Erdős problem 831

geometrypossible

declared openerdos:836

Erdős problem 836

graph theoryhypergraphschromatic numberN/A2 sources

declared openerdos:837

Erdős problem 837

graph theoryhypergraphsN/A

declared openerdos:838

Erdős problem 838

geometryconvexpossible

declared openerdos:839

Erdős problem 839

number theoryN/A

declared openerdos:840

Erdős problem 840

additive combinatoricssidon setsN/A

declared open · formalizederdos:849

True ↔ ∀ t ≥ 1, ∃ a, {n | ∃ k ≥ 1, 2 * k ≤ n ∧ n.choose k = a}.ncard = t

number theorybinomial coefficientsA003016 · A003015 · A059233 · A098565 · A090162 · A180058 · A1822372 sources

declared open · formalizederdos:850

True ↔ ∃ x y, x ≠ y ∧ x.primeFactors = y.primeFactors ∧ (x + 1).primeFactors = (y + 1).primeFactors ∧ (x + 2).primeFactors = (y + 2).primeFactors

number theoryprimesA3431013 sources

declared openerdos:852

Erdős problem 852

number theoryprimesA001223 · A053597 · A0785152 sources

declared open · formalizederdos:853

Filter.Tendsto Erdos853.r Filter.atTop Filter.atTop

number theoryprimesA001223 · A3907692 sources

declared openerdos:854

Erdős problem 854

number theoryA389839 · A048670

declared open · formalizederdos:855

True ↔ ∀ᶠ (x : ℕ) (y : ℕ) in Filter.atTop, (x + y).primeCounting ≤ x.primeCounting + y.primeCounting

number theoryprimesA0231932 sources

declared openerdos:856

Let

k\geq 3

and

f_k(N)

be the maximum of

\sum_{n\in A}\frac{1}{n}

over all

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

containing no

k

subsets with the same pairwise least common multiple. Estimate

f_k(N)

. The claimed answer:

f_k(N)=(\log N)^{\gamma_k+o(1)}

, where

\gamma_k

is a weighted generalization of the Tang-Zhang sunflower capacity.

number theorypossible3 sources

declared open · formalizederdos:857

have f := sorry; ∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun n => ↑(Erdos857.m n k) / f k n) Filter.atTop (nhds 1)

combinatoricspossible2 sources

declared open · formalizederdos:859

∃ c₁ > 0, ∃ c₂ > 0, ∃ d, (∀ t > 0, (Erdos859.DivisorSumSet t).HasDensity (d t)) ∧ Asymptotics.IsEquivalent Filter.atTop (fun t => d t) fun t => c₁ / Real.log ↑t ^ c₂

number theorydivisorsN/A2 sources

declared openerdos:860

Erdős problem 860

number theoryprimesA048670 · A058989

declared openerdos:864

Erdős problem 864

number theorysidon setsadditive combinatoricsA3891822 sources

declared openerdos:866

Estimate the least excess

g_k(N)

forcing

k

integers whose pairwise sums all lie in a dense subset of

\{1, \dots, 2N\}

; in particular, determine the positive variant

h_4(n)

number theoryadditive combinatoricspossible5 sources

declared openerdos:870

Let

k\geq 3

and

A

be an additive basis of order

k

. Does there exist a constant

c=c(k)>0

such that if

r(n)\geq c\log n

for all large

n

(where

r(n)

counts representations of

n

as a sum of at most

k

elements of

A

) then

A

must contain a minimal basis of order

k

? The claimed answer is no, for every

k\geq 3

number theoryadditive basisN/A3 sources

declared open · formalizederdos:872

True ↔ ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos872.L n) ≥ ε * ↑n

number theoryprimitive setspossible3 sources

declared open · formalizederdos:873

True ↔ ∀ (a : ℕ → ℕ), ∀ ε > 0, 0 < a 0 → StrictMono a → ∃ k, ∀ X > 0, ↑↑(Erdos873.F a X k) < ↑(X ^ ε)

number theoryN/A3 sources

declared openerdos:875

Erdős problem 875

additive combinatoricsN/A2 sources

declared openerdos:876

Erdős problem 876

additive combinatoricsN/A

declared openerdos:878

Erdős problem 878

number theoryA339378 · possible

declared openerdos:879

Erdős problem 879

number theoryA186736

declared open · formalizederdos:881

True ↔ ∀ (k : ℕ) (A : Set ℕ), Erdos881.IsMinimalAsymptoticAddBasisOfOrder k A → ∃ B ⊆ A, B.Infinite ∧ (A \ B).IsAsymptoticAddBasisOfOrder (k + 1)

number theoryadditive basisN/A2 sources

declared openerdos:883

Erdős problem 883

number theorygraph theoryN/A

declared open · formalizederdos:885

True ↔ ∀ k ≥ 1, ∃ Ns, (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = k ∧ (⋂ n ∈ Ns, Erdos885.factorDifferenceSet n).ncard ≥ k

number theorydivisorsN/A2 sources

declared open · formalizederdos:886

sorry ↔ ∀ ε > 0, ∃ K, ∀ᶠ (n : ℕ) in Filter.atTop, (Erdos886.Erdos886Divisors n ε 1).card ≤ K

number theorydivisorsN/A2 sources

declared open · formalizederdos:887

∀ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ sorry

number theorydivisorsN/A2 sources

declared open · formalizederdos:889

Filter.Tendsto Erdos889.v₀ Filter.atTop (nhds ⊤)

number theorypossible2 sources

declared open · formalizederdos:890

sorry ↔ ∀ k ≥ 1, Filter.liminf (fun n => ∑ i ∈ Finset.range k, ↑(Erdos890.omegaGt k (n + i))) Filter.atTop ≤ ↑k

number theoryprimesN/A2 sources

declared open · formalizederdos:891

True ↔ ∀ k ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m ∈ Finset.Ico n (n + ∏ i ∈ Finset.range k, Nat.nth Nat.Prime i), k < ArithmeticFunction.cardDistinctFactors m

number theoryN/A2 sources

declared openerdos:892

Erdős problem 892

number theoryprimitive setsN/A

declared open · formalizederdos:893

True ↔ Filter.Tendsto (fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n)) Filter.atTop Filter.atTop

number theorydivisorsA046801 · possible3 sources

declared openerdos:901

Erdős problem 901

combinatoricshypergraphspossible

declared openerdos:902

Erdős problem 902

graph theoryA362137

declared open · formalizederdos:906

Is there an entire non-zero function

f:\mathbb{C}\to \mathbb{C}

such that, for any infinite sequence

n_1<n_2<\cdots

, the set

\{ z: f^{(n_k)}(z)=0 \textrm{ for some }k\geq 1\}

is everywhere dense? The literal question is trivial for polynomials, so the claims address the transcendental entire case, in the affirmative.

analysisiterated functionsN/A5 sources

declared openerdos:911

Erdős problem 911

graph theoryramsey theoryN/A

declared open · formalizederdos:912

∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => c * (↑n / Real.log ↑n) ^ (1 / 2)

number theoryfactorialsA0716262 sources

declared open · formalizederdos:913

True ↔ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite

number theoryA3597472 sources

declared openerdos:917

Erdős problem 917

graph theorychromatic numberN/A

declared open · formalizederdos:918

True ↔ ∃ V G, Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph 1 → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0

graph theorychromatic numberN/A2 sources

declared openerdos:919

Erdős problem 919

graph theorychromatic numberN/A

declared openerdos:928

Erdős problem 928

number theoryA006530

Problems · Vela Mathematics Program

Problem ledger

Search problems.science