Vela Mathematics Program: problems

Problem ledger

1,217 problems · 8/25Number SourcesGraph view

declared proved (Lean) · formalizederdos:351

True ↔ ∀ (P : Polynomial ℚ), 0 < P.natDegree → 0 < P.leadingCoeff → Erdos351.HasCompleteImage P

number theorycomplete sequencesN/A6 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 proved (Lean) · formalizederdos:353

True ↔ ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → MeasureTheory.volume A = ⊤ → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, ∃ d ∈ A, EuclideanGeometry.IsIsoscelesTrapezoid a b c d ∧ MeasureTheory.volume ((convexHull ℝ) {a, b, c, d}) = 1

geometryN/A4 sources

declared open · formalizederdos:354

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

number theoryN/A2 sources

declared proved (Lean) · formalizederdos:355

True ↔ ∃ A, IsLacunary A ∧ ∃ u v, u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x | ∃ A', ∃ (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}

number theoryunit fractionsN/A5 sources

declared provederdos:356

Erdős problem 356

number theorypossible

declared open · formalizederdos:357

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

number theoryA364132 · A364153 · possible2 sources

declared proved · formalizederdos:358

True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTop

number theoryadditive basisprimespossible3 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 solvederdos:360

Erdős problem 360

number theorypossible

declared open · formalizederdos:361

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

number theorypossible2 sources

declared provederdos:362

Erdős problem 362

number theorypossible

declared disproved (Lean) · formalizederdos:363

False ↔ {S | Erdos363.IsValidCollection S}.Finite

number theoryN/A5 sources

declared verifiable · formalizederdos:364

¬∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful

number theoryA060355 · A0764452 sources

declared openerdos:365

Erdős problem 365

number theoryA060355 · A060859 · A175155

declared verifiable · formalizederdos:366

True ↔ ∃ n > 0, Nat.Full 2 n ∧ Nat.Full 3 (n + 1)

number theoryA0603553 sources

declared openerdos:367

Erdős problem 367

number theoryA0575213 sources

declared openerdos:368

Erdős problem 368

number theoryA0743993 sources

declared proved (Lean) · formalizederdos:369

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ (k : ℕ), 2 ≤ k → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε

number theoryN/A7 sources

declared proved (Lean) · formalizederdos:370

True ↔ {n | ↑n.maxPrimeFac < √↑n ∧ ↑(n + 1).maxPrimeFac < √(↑n + 1)}.Infinite

number theoryN/A5 sources

declared open · formalizederdos:371

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

number theoryA0700892 sources

declared provederdos:372

Erdős problem 372

number theoryA071870

declared open · formalizederdos:373

Erdos373.S.Finite

number theoryfactorialsA0031352 sources

declared openerdos:374

Erdős problem 374

number theoryA388851 · A387184 · A389117 · A3891482 sources

declared falsifiable · formalizederdos:375

True ↔ Erdos375.Erdos375Prop

number theoryN/A2 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 provederdos:378

Erdős problem 378

number theorybinomial coefficientsN/A

declared proved (Lean) · formalizederdos:379

Filter.limsup (fun n => ↑(Erdos379.S n)) Filter.atTop = ⊤

number theorybinomial coefficientspossible5 sources

declared provederdos:380

Erdős problem 380

number theoryA070003 · A388654 · A387054 · A3891003 sources

declared disprovederdos:381

Erdős problem 381

number theorydivisorsA002182

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 provederdos:384

Erdős problem 384

number theorybinomial coefficientsN/A

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 solved · formalizederdos:387

False ↔ ∃ c, 0 < c ∧ ∀ (n k : ℕ), 1 ≤ k → k < n → ∃ d, ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k

number theorybinomial coefficientsN/A2 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 provederdos:391

Erdős problem 391

number theoryfactorialsA034258 · A034259

declared proved (Lean) · formalizederdos:392

∀ (A : ℕ → ℕ), (∀ n > 0, IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n ^ 2), t + 1 = x} (A n)) → (fun n => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

number theoryfactorialspossible5 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 provederdos:395

Erdős problem 395

analysisN/A

declared open · formalizederdos:396

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

number theorybinomial coefficientsA3750773 sources

declared disproved (Lean) · formalizederdos:397

False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite

number theorybinomial coefficientsN/A7 sources

declared falsifiable · formalizederdos:398

sorry ↔ {n | ∃ m, n.factorial + 1 = m ^ 2} = {4, 5, 7}

number theoryfactorialsA146968 · A1413992 sources

declared disproved (Lean) · formalizederdos:399

False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)

number theoryfactorialsN/A5 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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science