Vela Mathematics Program: problems

Problem ledger

1,217 problems · 10/25Number SourcesGraph view

declared openerdos:451

n_k

be the least integer greater than

2k

for which

\prod_{i=1}^k (n_k - i)

has no prime factor in

(k, 2k)

. How rapidly must

n_k

grow?

number theoryA3866203 sources

declared openerdos:452

Erdős problem 452

number theorypossible

declared disproved (Lean) · formalizederdos:453

False ↔ Erdos453.EventuallyHasPrimeWitness

number theoryN/A5 sources

declared open · formalizederdos:454

True ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

number theoryprimesA389676 · A3896772 sources

declared open · formalizederdos:455

True ↔ ∀ (q : ℕ → ℕ), StrictMono q → (∀ (n : ℕ), Nat.Prime (q n) ∧ q (n + 2) - q (n + 1) ≥ q (n + 1) - q n) → Filter.Tendsto (fun n => ↑(q n) / ↑n ^ 2) Filter.atTop Filter.atTop

number theoryN/A2 sources

declared open · formalizederdos:456

True ↔ Filter.Tendsto (fun N => ↑(Nat.count {n | Erdos456.m n < Erdos456.p n} N) / ↑N) Filter.atTop (nhds 1)

number theoryA034694 · A061026 · possible3 sources

declared proved (Lean) · formalizederdos:457

True ↔ ∃ ε > 0, {n | ∀ (p : ℕ), ↑p ≤ (2 + ε) * Real.log ↑n → Nat.Prime p → p ∣ ∏ i ∈ Finset.Icc 1 ⌊Real.log ↑n⌋₊, (n + i)}.Infinite

number theoryA3916686 sources

declared falsifiable · formalizederdos:458

True ↔ ∀ (k : ℕ), Erdos458.lcm_upto (Nat.nth Prime (k + 1) - 1) < Nat.nth Prime k * Erdos458.lcm_upto (Nat.nth Prime k)

number theoryprimesA0566042 sources

declared solved (Lean) · formalizederdos:459

∀ {u : ℕ}, 2 ≤ u → u + 2 ≤ Erdos459.f u ∧ Erdos459.f u ≤ u ^ 2

number theoryprimesA2892805 sources

declared openerdos:460

Erdős problem 460

number theoryN/A2 sources

declared openerdos:461

Erdős problem 461

number theoryprimespossible

declared openerdos:462

Erdős problem 462

number theoryprimesA032742 · possible

declared open · formalizederdos:463

True ↔ ∃ f, ∃ (_ : Filter.Tendsto f Filter.atTop Filter.atTop), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m, m.Composite ∧ n + f n < m ∧ m < n + m.minFac

number theoryprimespossible2 sources

declared proved (Lean) · formalizederdos:464

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (k : ℕ), 0 < n k) → IsLacunary n → ∃ θ, Irrational θ ∧ ¬Dense (Set.range fun k => ↑(θ * ↑(n k)))

number theoryN/A4 sources

declared provederdos:465

Erdős problem 465

number theoryN/A

declared provederdos:466

Erdős problem 466

number theoryN/A

declared openerdos:467

Erdős problem 467

number theoryN/A

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

Erdős problem 471

number theorypossible

declared openerdos:472

Erdős problem 472

number theoryA389713 · possible

declared provederdos:473

Erdős problem 473

number theoryA055265

declared not provable · $100erdos:474

Erdős problem 474

set theoryramsey theoryN/A

declared decidableerdos:475

Erdős problem 475

number theoryadditive combinatoricsN/A

declared proved (Lean) · formalizederdos:476

True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (A : Finset (ZMod p)), A.restrictedSumset.card ≥ min (2 * A.card - 3) p

number theoryadditive combinatoricsN/A5 sources

declared open · formalizederdos:477

Does there exist an integer polynomial

f

of degree at least two and a set

A \subseteq \mathbb{Z}

such that every integer has a unique representation

n = a + f(k)

? A manuscript claims the thirteenth powers admit a tiling complement.

number theoryN/A4 sources

declared openerdos:478

Erdős problem 478

number theoryfactorialsA210184

declared open · formalizederdos:479

sorry ↔ ∀ k > 1, {n | 2 ^ n ≡ k [MOD n]}.Infinite

number theoryA036236 · A015919 · A050259 · A015921 · A006521 · A006517 · A0159402 sources

declared proved · formalizederdos:480

True ↔ ∀ (x : ℕ → ℝ), (∀ (n : ℕ), x n ∈ Set.Icc 0 1) → ⨅ n, Filter.liminf (fun m => ↑↑n * |x (m + ↑n) - x m|) Filter.atTop ≤ 1 / √5

number theoryN/A3 sources

declared proved (Lean) · formalizederdos:481

∀ {r : ℕ} (a b : Fin r → ℕ), (∀ (i : Fin r), 0 < a i) → 1 < ∑ i, 1 / ↑(a i) → ∃ k, ¬((Erdos481.T a b)^[k] [1]).Nodup

number theoryN/A5 sources

declared solvederdos:482

Erdős problem 482

number theoryA004539

declared openerdos:483

Erdős problem 483

number theoryadditive combinatoricsramsey theoryA030126

declared proved (Lean) · formalizederdos:484

∃ c, 0 < c ∧ ∀ (k : ℕ), 0 < k → ∃ N₀, ∀ (N : ℕ), N₀ ≤ N → ∀ (f : ℕ → Fin k), c * ↑N ≤ ↑{n ∈ Finset.Icc 1 N | ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n}.card

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared provederdos:485

Erdős problem 485

analysispolynomialspossible2 sources

declared open · formalizederdos:486

True ↔ ∀ (X : (n : ℕ) → Set (ZMod n)), ∃ d, {m | ∀ (n : ℕ), ↑m ∉ X n}.HasLogDensity d

number theoryprimitive setsN/A2 sources

declared proved (Lean) · formalizederdos:487

True ↔ ∀ (A : Set ℕ), A.HasPosDensity → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ b ≠ c ∧ a ≠ c ∧ a.lcm b = c

number theoryN/A5 sources

declared falsifiable · formalizederdos:488

True ↔ ∀ (A : Finset ℕ), A.Nonempty → 0 ∉ A → 1 ∉ A → ∀ (n m : ℕ), m > n → A.max ≤ ↑n → ↑{x ∈ Finset.Icc 1 m | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑m < 2 * ↑{x ∈ Finset.Icc 1 n | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑n

number theoryN/A3 sources

declared open · formalizederdos:489

A

is a forbidden-divisor set with

|A \cap [1,x]| = o(\sqrt{x})

and

B = \{b_1 < b_2 < \cdots\}

the sifted set, must

x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2

converge to a finite limit?

number theoryN/A4 sources

declared proved (Lean)erdos:490

Erdős problem 490

number theoryA3972054 sources

declared provederdos:491

Erdős problem 491

number theoryN/A

declared disprovederdos:492

Erdős problem 492

number theoryN/A

declared proved (Lean) · formalizederdos:493

True ↔ ∃ k N, ∀ (n : ℤ), N ≤ n → ∃ a, (∀ (i : Fin k), 2 ≤ a i) ∧ ∏ i, a i - ∑ i, a i = n

number theoryN/A5 sources

declared proved · formalizederdos:494

∀ (k card p : ℕ), Nat.Prime p → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494.Erdos494Unique k card

analysisadditive combinatoricsN/A2 sources

declared open · formalizederdos:495

True ↔ ∀ (α β : ℝ), Filter.liminf (fun n => ↑n * distToNearestInt (↑n * α) * distToNearestInt (↑n * β)) Filter.atTop = 0

diophantine approximationnumber theoryN/A2 sources

declared provederdos:496

Erdős problem 496

number theorydiophantine approximationN/A

declared solved (Lean) · formalizederdos:497

∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(DedekindNumber.M' n) = 2 ^ ((1 + o n) * ↑(n.choose (n / 2)))

combinatoricsA0003725 sources

declared proved (Lean) · formalizederdos:498

True ↔ ∀ (n : ℕ) (z : Fin n → ℂ), (∀ (i : Fin n), 1 ≤ ‖z i‖) → ∀ (c : ℂ), {ε | (∀ (i : Fin n), ε i = -1 ∨ ε i = 1) ∧ ∑ i, ↑(ε i) * z i ∈ Metric.ball c 1}.ncard ≤ n.choose (n / 2)

combinatoricsanalysisN/A5 sources

declared proved (Lean) · formalizederdos:499

True ↔ ∀ (n : ℕ), ∀ M ∈ doublyStochastic ℝ (Fin n), ∃ σ, ↑n ^ (-↑n) ≤ ∏ i, M i (σ i)

combinatoricsN/A5 sources

declared open · $500erdos:500

Erdős problem 500

graph theoryhypergraphsturan numberA140462

Problems · Vela Mathematics Program

Problem ledger

Search problems.science