Vela Mathematics Program: problems

Problem ledger

declared open · formalizederdos:18

∀ᶠ (n : ℕ) in Filter.atTop, Erdos18.practicalH n.factorial < n

number theorydivisorsfactorialsA0051532 sources

declared disproved (Lean) · formalizederdos:26

A\subset\mathbb{N}

be infinite. Must there exist some

k\geq 1

such that almost all integers have a divisor of the form

a+k

for some

a\in A

? The question as posed follows negatively from Davenport–Erdős (1951). The AI result settles Tenenbaum's harder variant, also negatively: there is an infinite

A

such that for every

k\geq 1

the set of multiples of

A+k

has upper density below

0.34

number theorydivisorsN/A6 sources

declared proved · $250erdos:144

Erdős problem 144

number theorydivisorsA005279

declared disprovederdos:381

Erdős problem 381

number theorydivisorsA002182

declared provederdos:444

Erdős problem 444

number theorydivisorsN/A

declared solvederdos:446

Erdős problem 446

number theorydivisorsA074738

declared disproved · formalizederdos:448

False ↔ ∀ (ε : ℝ), 0 < ε → {n | ↑(Erdos448.tauPlus n) < ε * ↑n.divisors.card}.HasDensity 1

number theorydivisorsA3974332 sources

declared disprovederdos:449

Erdős problem 449

number theorydivisorspossible

declared open · formalizederdos:450

How large must

y(\varepsilon, n)

be so that every interval

(x, x+y)

contains at most

\varepsilon y

integers having a divisor in

(n, 2n)

? The candidate proof gives the sharp fixed-

\varepsilon

order

y = \Theta_\varepsilon(n)

, uniformly in the translate.

number theorydivisorsN/A4 sources

declared openerdos:468

Erdős problem 468

number theorydivisorsA167485 · A387502 · A387503

declared proved (Lean) · formalizederdos:469

Does the sum of the reciprocals of all primitive pseudoperfect numbers converge?

number theorydivisorsA006036 · A119425 · possible5 sources

declared open · formalized · $10erdos:470

sorry ↔ ∃ n, n.Weird ∧ Odd n

number theorydivisorsA006037 · A0029752 sources

declared provederdos:673

Erdős problem 673

number theorydivisorsN/A

declared disproved (Lean) · formalizederdos:692

False ↔ ∀ (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → ∀ (n : ℕ), UnimodularOn (δ n) (n + 1)

number theorydivisorsN/A5 sources

declared openerdos:693

Erdős problem 693

number theorydivisorsA391118 · possible

declared solved (Lean)erdos:696

Erdős problem 696

number theorydivisorspossible4 sources

declared proved · formalizederdos:697

∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

number theorydivisorsN/A2 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 disproved (Lean) · formalizederdos:884

False ↔ Erdos884.Erdos884Prop

number theorydivisorsN/A3 sources

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:893

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

number theorydivisorsA046801 · possible3 sources

declared open · formalizederdos:945

True ↔ Erdos945.Erdos945Prop

number theorydivisorspossible · A0488922 sources

declared proved · formalizederdos:946

{n | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 1)}.Infinite

number theorydivisorsA005237 · A2847832 sources

declared proved (Lean)erdos:964

Erdős problem 964

number theorydivisorsN/A4 sources

declared open · formalizederdos:975

True ↔ ∀ (f : Polynomial ℤ), f.natDegree ≠ 0 → Irreducible f → (∀ᶠ (n : ℤ) in Filter.atTop, 1 ≤ Polynomial.eval n f) → ∃ c > 0, Filter.Tendsto (fun x => Erdos975.Erdos975Sum f x / (x * Real.log x)) Filter.atTop (nhds c)

number theorydivisorsA147807 · possible2 sources

declared open · formalizederdos:1054

sorry ↔ (fun n => ↑(Erdos1054.f n)) =o[Filter.atTop] fun n => ↑n

number theorydivisorsA1674853 sources

declared provederdos:1099

Erdős problem 1099

number theorydivisorsN/A

declared openerdos:1100

Erdős problem 1100

number theorydivisorsA325864 · possible2 sources

declared provederdos:1217

Erdős problem 1217

number theorydivisorsprimitive setsN/A3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science