Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 3/12Number SourcesGraph view

declared openerdos:278

Erdős problem 278

number theorycovering systemsN/A

declared open · formalizederdos:279

True ↔ ∀ k ≥ 3, ∃ a N, (∀ (p : ℕ), Nat.Prime p → a p < p) ∧ ∀ n ≥ N, ∃ p, ∃ t ≥ k, Nat.Prime p ∧ n = a p + t * p

number theorycovering systemsprimesN/A2 sources

declared disproved (Lean) · formalizederdos:280

False ↔ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 1 ≤ i → a i < n i) → (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) → ¬Filter.Tendsto (fun k => ↑(Erdos280.uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)

number theorycovering systemsN/A5 sources

declared proved (Lean) · formalizederdos:281

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε

number theorycovering systemsN/A7 sources

declared open · formalizederdos:282

∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Odd x.den → Erdos282.greedyUnitFractionRem {n | Odd n} x =ᶠ[Filter.atTop] 0

number theoryunit fractionsN/A2 sources

declared proved (Lean) · formalizederdos:283

True ↔ ∀ (p : Polynomial ℤ), Erdos283.Condition p

number theoryunit fractionsA3807916 sources

declared provederdos:284

Erdős problem 284

number theoryunit fractionspossible

declared proved · formalizederdos:285

True ↔ ∀ (f : ℕ → ℕ) (S : Set ℕ), S = {k | ∃ n, StrictMono n ∧ 0 ∉ Set.range n ∧ 1 = ∑ i, 1 / ↑(n i)} → (∀ k ∈ S, IsLeast {x | ∃ n, ∃ (_ : StrictMono n) (_ : 0 ∉ Set.range n) (_ : 1 = ∑ i, 1 / ↑(n i)), n (Fin.last k) = x} (f k)) → ∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ k ∈ S, ↑(f k) = (1 + o k) * Real.exp 1 / (Real.exp 1 - 1) * (↑k + 1)

number theoryunit fractionsA0306592 sources

declared provederdos:286

Erdős problem 286

number theoryunit fractionsN/A

declared falsifiable · formalizederdos:287

True ↔ ∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ), StrictMono s → 1 < s ⟨0, ⋯⟩ → ∑ i, 1 / ↑(s i) = 1 → 3 ≤ Erdos287.max_gap k s

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:288

sorry ↔ {I | ∀ (j : Fin 2), (I j).1 ≤ (I j).2 ∧ ∃ n, ∑ j, ∑ nⱼ ∈ (Set.Icc (I j).1 (I j).2).toFinset, (↑↑nⱼ)⁻¹ = ↑↑n}.Finite

number theoryunit fractionsN/A3 sources

declared open · formalizederdos:289

True ↔ ∀ᶠ (k : ℕ) in Filter.atTop, ∃ I, (∀ (i : Fin k), (I i).1 < (I i).2) ∧ (∀ (i j : Fin k), i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧ ∑ i, ∑ n ∈ Finset.Icc (I i).1 (I i).2, (↑n)⁻¹ = 1

number theoryunit fractionsN/A2 sources

declared proved (Lean) · formalizederdos:290

True ↔ ∀ (a : ℕ), 1 ≤ a → ∃ b, a < b ∧ Erdos290.harmonicDen a (b + 1) < Erdos290.harmonicDen a b

number theoryunit fractionsA3750815 sources

declared open · formalizederdos:291

Erdos291.L 1 = 1 ∧ Erdos291.L 2 = 2 ∧ Erdos291.L 3 = 6 ∧ Erdos291.L 4 = 12

number theoryunit fractionsA1105663 sources

declared provederdos:292

Erdős problem 292

number theoryunit fractionsA092671

declared openerdos:293

Erdős problem 293

number theoryunit fractionspossible

declared provederdos:294

Erdős problem 294

number theoryunit fractionspossible

declared open · formalizederdos:295

sorry ↔ Filter.Tendsto (fun N => ↑(Erdos295.k N) - (Real.exp 1 - 1) * ↑N) Filter.atTop Filter.atTop

number theoryunit fractionsA1928812 sources

declared proved (Lean) · formalizederdos:296

(∀ (N k : ℕ), Erdos296.HasDisjointUnitDecomps N k → ↑k ≤ Erdos296.recipSum (Finset.Icc 1 N)) ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∀ᶠ (N : ℕ) in Filter.atTop, Erdos296.HasDisjointUnitDecomps N ⌊(1 - ε) * Real.log ↑N⌋₊

number theoryunit fractionspossible5 sources

declared solvederdos:297

Erdős problem 297

number theoryunit fractionsA092670

declared proved (Lean) · formalizederdos:298

True ↔ ∀ (A : Set ℕ), 0 ∉ A → 0 < A.upperDensity → ∃ S, ↑S ⊆ A ∧ ∑ n ∈ S, 1 / ↑n = 1

number theoryunit fractionsN/A4 sources

declared disproved (Lean) · formalizederdos:299

False ↔ ∃ a, StrictMono a ∧ (∀ (n : ℕ), 0 < a n) ∧ (fun n => ↑(a (n + 1)) - ↑(a n)) =O[Filter.atTop] 1 ∧ ∀ (S : Finset ℕ), ∑ i ∈ S, 1 / ↑(a i) ≠ 1

number theoryunit fractionsN/A4 sources

declared solvederdos:300

Erdős problem 300

number theoryunit fractionsA390393

declared openerdos:301

Erdős problem 301

number theoryunit fractionsA390394

declared open · formalizederdos:302

∀ (f : ℕ → ℕ), (∀ (N : ℕ), Erdos302.IsMaxNoTripleCard N (f N)) → Filter.Tendsto (fun N => ↑(f N) / ↑N) Filter.atTop (nhds sorry)

number theoryunit fractionsA3903953 sources

declared proved (Lean) · formalizederdos:303

True ↔ ∀ (𝓒 : ℤ → ℤ), (Set.range 𝓒).Finite → ∃ a b c, [a, b, c, 0].Nodup ∧ 1 / ↑a = 1 / ↑b + 1 / ↑c ∧ (𝓒 '' {a, b, c}).Subsingleton

number theoryunit fractionsN/A5 sources

declared open · formalizederdos:304

∀ {a b : ℕ}, 1 ∈ Erdos304.unitFractionExpressible a b → a ∣ b

number theoryunit fractionsA097847 · A0978492 sources

declared provederdos:305

Erdős problem 305

number theoryunit fractionspossible

declared open · formalizederdos:306

a/b \in \mathbb{Q}_{>0}

and

b

is squarefree, can

a/b

always be written as a finite sum of reciprocals of distinct products of two distinct primes?

number theoryunit fractionsN/A4 sources

declared verifiable · formalizederdos:307

sorry ↔ ∃ P Q, (∀ p ∈ P, Nat.Prime p) ∧ (∀ q ∈ Q, Nat.Prime q) ∧ 1 = (∑ p ∈ P, (↑p)⁻¹) * ∑ q ∈ Q, (↑q)⁻¹

number theoryunit fractionsN/A2 sources

declared provederdos:308

Erdős problem 308

number theoryunit fractionspossible

declared disprovederdos:309

Erdős problem 309

number theoryunit fractionsA217693

declared provederdos:310

Erdős problem 310

number theoryunit fractionsN/A

declared openerdos:311

Erdős problem 311

number theoryunit fractionsN/A

declared open · formalizederdos:312

True ↔ ∃ c, 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ N₀, ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K → ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:313

sorry ↔ Erdos313.erdos313Solutions.Infinite

number theoryunit fractionsA0543772 sources

declared proved (Lean) · formalizederdos:314

True ↔ Filter.liminf (fun n => ↑n ^ 2 * Erdos314.epsilon n) Filter.atTop = 0

number theoryunit fractionsN/A5 sources

declared proved (Lean) · formalizederdos:315

True ↔ ∀ (a : ℕ → ℕ), (∀ (i : ℕ), 0 < a i) → StrictMono a → (∃ i, a i ≠ Erdos315.u i + 1) → ∑' (i : ℕ), 1 / ↑(a i) = 1 → Filter.liminf (fun i => ↑(a i) ^ (1 / 2) ^ (i + 1)) Filter.atTop < Erdos315.c₀

number theoryunit fractionsA000058 · A0763935 sources

declared disproved (Lean) · formalizederdos:316

False ↔ ∀ (A : Finset ℕ), 0 ∉ A → 1 ∉ A → ∑ n ∈ A, 1 / ↑n < 2 → ∃ A₁ A₂, Disjoint A₁ A₂ ∧ A = A₁ ∪ A₂ ∧ ∑ n ∈ A₁, 1 / ↑n < 1 ∧ ∑ n ∈ A₂, 1 / ↑n < 1

number theoryunit fractionsN/A4 sources

declared open · formalizederdos:317

∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| ≥ 1 / ↑((Finset.Icc 1 n).lcm id)

number theoryunit fractionsN/A2 sources

declared solved · formalizederdos:318

∃ A, A.HasPosDensity ∧ ¬Erdos318.P₁ A

number theoryunit fractionsN/A2 sources

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 solvederdos:320

Let

S(N)

count the distinct values of

\sum_{n\in A} 1/n

over

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

. Estimate

S(N)

number theoryunit fractionsA0722072 sources

declared solved · formalizederdos:321

What is the largest

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

such that all subset sums

\sum_{n\in S}1/n

(over

S\subseteq A

) are distinct?

number theoryunit fractionsA384927 · A3915923 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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science