Vela Mathematics Program: problems

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 4/13Number SourcesGraph view

declared open · formalizederdos:319

∀ (N : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A ⊆ Finset.Icc 1 N) (_ : ∃ δ, ∑ n ∈ A, ↑↑(δ n) / ↑n = 0 ∧ ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', ↑↑(δ n) / ↑n ≠ 0), A.card = x} sorry

number theoryunit fractionspossible2 sources

declared openerdos:322

Erdős problem 322

number theorypowersA025456 · A025418

declared open · formalizederdos:323

True ↔ ∀ k ≥ 1, ∀ ε > 0, (fun x => ↑x ^ (1 - ε)) =O[Filter.atTop] fun x => ↑(Erdos323.f k k x)

number theorypowersA004825 · A004831 · A004832 · A004833 · A004842 · A004843 · A004844 · A004845 · A004857 · A004869 · possible2 sources

declared open · formalizederdos:324

sorry ↔ ∃ f, Set.InjOn (fun x => match x with | (a, b) => Polynomial.eval (↑a) f + Polynomial.eval (↑b) f) {(a, b) | a < b}

number theorypowersN/A2 sources

declared open · formalizederdos:325

True ↔ ∀ (k : ℕ), 3 ≤ k → (fun x => ↑x ^ (3 / ↑k)) =O[Filter.atTop] fun x => ↑(Erdos325.cardIsSumThreePowerBelow k x)

number theorypowersA004825 · A004832 · A004843 · A004854 · A004865 · possible2 sources

declared open · formalizederdos:326

Does there exist

A=\{a_1<a_2<\cdots\}\subset \mathbb{N}

which is a minimal basis of order

2

(every large integer is the sum of

2

elements from

A

, and no proper subset of

A

has this property) such that

\lim_{k\to \infty}a_k/k^2=c

for some

c\neq 0

? A claimed construction gives a minimal basis with

A(x)=C\sqrt{x}+O(1)

, answering the question affirmatively; Erdős and Graham had conjectured a negative answer.

number theoryadditive basisN/A4 sources

declared openerdos:327

Erdős problem 327

number theoryunit fractionsA3849272 sources

declared open · formalizederdos:329

sSup {x | ∃ A, ∃ (_ : IsSidon A), Erdos329.sidonUpperDensity A = x} = sorry

number theorypossible2 sources

declared open · formalizederdos:332

∀ (A : Set ℕ), sorry A → Erdos332.HasBoundedGaps (Erdos332.D_A A)

number theoryN/A3 sources

declared openerdos:334

Erdős problem 334

number theoryA062241 · A045535

declared openerdos:335

Erdős problem 335

number theoryadditive combinatoricsN/A2 sources

declared openerdos:336

h(r)

is the maximal finite exact order attainable by an additive basis of order at most

r

, what is

\lim_{r \to \infty} h(r)/r^2

? The candidate proof identifies the sharp limit

1/3

number theoryadditive basispossible2 sources

declared openerdos:338

Erdős problem 338

number theoryadditive basisN/A

declared open · formalizederdos:340

∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard

number theoryadditive combinatoricssidon setsA080200 · A0052822 sources

declared open · formalizederdos:341

True ↔ ∀ (a : ℕ → ℤ), (∀ᶠ (n : ℕ) in Filter.atTop, IsLeast {x | a n < x ∧ x ∉ {x | ∃ i ≤ n, ∃ j ≤ n, a i + a j = x}} (a (n + 1))) → have d := fun i => a (i + 1) - a i; ∃ p > 0, ∀ᶠ (m : ℕ) in Filter.atTop, d (m + p) = d m

number theoryN/A2 sources

declared open · formalizederdos:342

sorry ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → {n | ∃ m, a m = a n + 2}.Infinite

number theoryA0028583 sources

declared openerdos:345

Erdős problem 345

number theorycomplete sequencesA0016612 sources

declared open · formalizederdos:346

Let

A=\{1\leq a_1< a_2<\cdots\}

be a set of integers such that

A\backslash B

is complete for any finite subset

B

and not complete for any infinite subset

B

. If

a_{n+1}/a_n \geq 1+\epsilon

for all

n

, must

\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2

? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

number theorycomplete sequencesN/A4 sources

declared open · formalizederdos:348

{x | ∃ m n, ∃ (_ : m < n), ∃ a, ∃ (_ : Monotone a) (_ : ∀ (s : Finset ℕ), s.card = m → IsAddComplete (Set.range (Function.updateFinset a s 0))) (_ : ∀ (t : Finset ℕ), t.card = n → ¬IsAddComplete (Set.range (Function.updateFinset a t 0))), (m, n) = x} = sorry

number theorycomplete sequencesN/A2 sources

declared open · formalizederdos:349

∀ (t α : ℝ), 0 < t → 2 < α → ¬Erdos349.IsGoodPair t α

number theorycomplete sequencesN/A3 sources

declared open · formalizederdos:352

True ↔ ∃ c > 0, ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → ↑(MeasureTheory.volume A) ≥ ↑c → ∃ t, (∀ (p : Fin 3), t.points p ∈ A) ∧ EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1

geometryN/A3 sources

declared open · formalizederdos:354

True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2)

number theoryN/A2 sources

declared open · formalizederdos:357

(fun n => ↑(Erdos357.f n)) =o[Filter.atTop] fun n => ↑n

number theoryA364132 · A364153 · possible2 sources

declared open · formalizederdos:359

∀ (A : ℕ → ℕ), Erdos359.IsGoodFor A 1 → Filter.Tendsto (fun k => ↑(A k) / ↑k) Filter.atTop Filter.atTop

number theoryA0020482 sources

declared open · formalizederdos:361

∀ (c : ℝ), 0 < c → Erdos361.subsetSumAvoidanceNumber c = sorry

number theorypossible2 sources

declared openerdos:365

Erdős problem 365

number theoryA060355 · A060859 · A175155

declared openerdos:367

Erdős problem 367

number theoryA0575213 sources

declared openerdos:368

Erdős problem 368

number theoryA0743993 sources

declared open · formalizederdos:371

{n | (n + 1).maxPrimeFac > n.maxPrimeFac}.HasDensity (1 / 2)

number theoryA0700892 sources

declared open · formalizederdos:373

Erdos373.S.Finite

number theoryfactorialsA0031352 sources

declared openerdos:374

Erdős problem 374

number theoryA388851 · A387184 · A389117 · A3891482 sources

declared open · formalizederdos:376

True ↔ {n | n.centralBinom.Coprime 105}.Infinite

number theorybinomial coefficientsbase representationsA0309792 sources

declared open · formalizederdos:377

True ↔ ∃ C > 0, ∀ (n : ℕ), Erdos377.sumInvPrimesNotDvdCentralBinom n ≤ C

number theorybinomial coefficientsN/A2 sources

declared openerdos:382

Erdős problem 382

number theoryA388850

declared open · formalizederdos:383

True ↔ ∀ (k : ℕ), {p | Nat.Prime p ∧ (∏ i ∈ Finset.Icc 0 k, (p ^ 2 + i)).maxPrimeFac = p}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:385

sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, n < Erdos385.F n

number theoryA3222922 sources

declared open · formalizederdos:386

True ↔ ∃ k ≥ 2, ∃ᶠ (n : ℕ) in Filter.atTop, k ≤ n - 2 ∧ ∃ p q, n.choose k = ∏ i ∈ Finset.Ico p q, Nat.nth Nat.Prime i

number theorybinomial coefficientsA2809922 sources

declared openerdos:388

Erdős problem 388

number theoryN/A2 sources

declared open · formalizederdos:389

True ↔ ∀ n ≥ 1, ∃ k ≥ 1, ∏ i ∈ Finset.range k, (n + i) ∣ ∏ i ∈ Finset.range k, (n + k + i)

number theoryA3750712 sources

declared open · formalizederdos:390

Let

f(n)

be the least

m

for which

n!

can be written as

a_1\cdots a_k

with

n < a_1 < \cdots < a_k = m

- the smallest possible largest factor in a factorization of

n!

into distinct integers all exceeding

n

. Erdős, Guy and Selfridge proved

f(n) - 2n \asymp n/\log n

. Erdős asked whether there is a constant

c

with

f(n) - 2n \sim c\,\frac{n}{\log n},

and what it is. This preprint answers yes and names the constant:

\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.

number theoryfactorialsA1934294 sources

declared openerdos:393

Erdős problem 393

number theoryfactorialsA3883022 sources

declared open · formalizederdos:394

For the least

t_k(n)

with

n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1)

, do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with

c = 1/2048

admissible in the

t_2

bound.

number theoryA3440054 sources

declared open · formalizederdos:396

True ↔ ∀ (k : ℕ), ∃ n, n.descFactorial (k + 1) ∣ n.centralBinom

number theorybinomial coefficientsA3750773 sources

declared open · formalizederdos:400

True ↔ ∀ k ≥ 2, ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x => c * ↑x * Real.log ↑x

number theoryfactorialspossible3 sources

declared openerdos:404

Erdős problem 404

number theoryfactorialsN/A

declared open · formalizederdos:406

True ↔ {n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1]}.Finite

number theorybase representationsN/A2 sources

declared openerdos:408

Erdős problem 408

number theoryiterated functionsA049108

declared open · formalizederdos:409

∀ (n : ℕ), 0 < n → IsLeast {i | Nat.Prime ((fun x => x.totient + 1)^[i] n)} sorry

number theoryiterated functionsA039651 · A2294872 sources

declared open · formalizederdos:410

True ↔ ∀ n > 1, Filter.Tendsto (fun k => ↑((⇑(ArithmeticFunction.sigma 1))^[k] n) ^ (1 / ↑k)) Filter.atTop Filter.atTop

number theoryiterated functionsA007497 · possible2 sources

declared openerdos:411

Erdős problem 411

number theoryiterated functionsA383044 · possible2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science