Vela Mathematics Program: problems

Problem ledger

1,217 problems · 6/25Number SourcesGraph view

declared open · formalizederdos:251

True ↔ Irrational (∑' (n : ℕ), ↑(Nat.nth Nat.Prime n) / 2 ^ n)

number theoryirrationalityA0989903 sources

declared open · formalizederdos:252

True ↔ ∀ k ≥ 1, Irrational (Erdos252.erdos_252_sum k)

number theoryirrationalityA227988 · A227989 · A307036 · A359060 · possible2 sources

declared disproved · formalizederdos:253

¬∀ (a : ℕ → ℕ), 0 < a 0 → Erdos253.RepresentsAPs a → Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 1) → subsetSums (Set.range a) ∈ Filter.cofinite

number theoryN/A2 sources

declared open · formalizederdos:254

A \subseteq \mathbb{N}

has unbounded dyadic-shell counts and

\sum_{n \in A} \|\theta n\| = \infty

for every

0 < \theta < 1

, must

A

be complete - is every sufficiently large integer a sum of distinct elements of

A

number theoryN/A4 sources

declared provederdos:255

Erdős problem 255

discrepancyN/A

declared openerdos:256

Erdős problem 256

analysisN/A

declared open · formalizederdos:257

True ↔ ∀ (A : Set ℕ), A.Infinite → Irrational (∑' (n : ↑A), 1 / (2 ^ ↑n - 1))

irrationalityN/A2 sources

declared proved (Lean) · formalizederdos:258

True ↔ ∀ (a : ℕ → ℕ), (∀ (n : ℕ), 2 ≤ a n) → Filter.Tendsto a Filter.atTop Filter.atTop → Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / ↑(∏ i ∈ Finset.Icc 1 (n + 1), a i))

irrationalityN/A6 sources

declared proved (Lean) · formalizederdos:259

Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.moebius n) ^ 2 * ↑n / 2 ^ n)

irrationalityA3711345 sources

declared open · formalizederdos:260

sorry ↔ ∀ (a : ℕ → ℤ) (s : ℝ), StrictMono a → Filter.Tendsto (fun n => ↑(a n) / ↑n) Filter.atTop Filter.atTop → HasSum (fun n => ↑(a n) / 2 ^ a n) s → Irrational s

irrationalityN/A2 sources

declared openerdos:261

Erdős problem 261

number theoryN/A

declared solvederdos:262

Erdős problem 262

irrationalityN/A

declared open · formalizederdos:263

sorry ↔ Erdos263.IsIrrationalitySequence fun n => 2 ^ 2 ^ n

irrationalityN/A3 sources

declared open · formalizederdos:264

¬Erdos264.IsIrrationalitySequence fun x => 2 ^ x

irrationalityN/A4 sources

declared openerdos:265

Erdős problem 265

irrationalityN/A

declared disproved · formalizederdos:266

¬∀ (a : ℕ → ℕ), ((∀ (n : ℕ), a n ≥ 1) ∧ Summable fun x => 1 / ↑(a x)) → ∃ t ≥ 1, Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑t))

irrationalityN/A2 sources

declared open · formalizederdos:267

n_1 < n_2 < \cdots

with

n_{k+1}/n_k \ge c > 1

, must

\sum_k 1/F_{n_k}

be irrational? The proposed proof closes the range

1 < c < 2

left open by earlier criteria.

irrationalityN/A4 sources

declared proved (Lean) · formalizederdos:268

∀ (d : ℕ), (interior {x | ∃ A, A.Infinite ∧ (Summable fun n => 1 / ↑↑n) ∧ x = fun i => ∑' (n : ↑A), 1 / (↑↑n + ↑↑i)}).Nonempty

number theoryN/A5 sources

declared open · formalizederdos:269

∀ (P : Set ℕ), (∀ p ∈ P, Nat.Prime p) → P.Infinite → Irrational (Erdos269.series P)

irrationalityN/A2 sources

declared disprovederdos:270

For integers

a\geq1

and

b\geq1-a

, the series

C_{a,b}=\sum_{n=1}^{\infty} n!/((a+1)n+b)!

is transcendental. Equivalently, the series in Erdős Problem 270 is transcendental whenever

f(n)=an+b

is a positive integer-valued affine function.

irrationalityA0730162 sources

declared openerdos:271

Erdős problem 271

additive combinatoricsarithmetic progressionsA005487

declared open · formalizederdos:272

Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos272.maxArithInterCard N)) sorry

additive combinatoricsarithmetic progressionspossible2 sources

declared open · formalizederdos:273

True ↔ ∃ c, ∀ (i : c.ι), ∃ p, Nat.Prime p ∧ 5 ≤ p ∧ c.moduli i = Ideal.span {↑(p - 1)}

number theorycovering systemsN/A2 sources

declared open · formalizederdos:274

sorry ↔ ∀ (G : Type u_1) [inst : Group G], 1 < ENat.card G → ∀ (ι : Type u_2) [inst_1 : Fintype ι] (P : Erdos274.Group.ExactCovering G ι), 1 < Fintype.card ι → ∃ i j, i ≠ j ∧ Cardinal.mk ↥(P.parts i) = Cardinal.mk ↥(P.parts j)

group theorycovering systemsN/A3 sources

declared proved (Lean) · formalizederdos:275

∀ (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ), (∃ k, ∀ x ∈ Set.Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD ↑(n i)]) → ∀ (x : ℤ), ∃ i, x ≡ a i [ZMOD ↑(n i)]

number theorycovering systemsN/A5 sources

declared open · formalizederdos:276

True ↔ ∃ a, Erdos276.IsLucasSequence a ∧ (∀ (k : ℕ), (a k).Composite) ∧ ∀ n > 1, ∃ k, n.gcd (a k) = 1

number theorycovering systemsN/A2 sources

declared proved · formalizederdos:277

True ↔ ∀ (c : ℝ), ∃ n, ↑((ArithmeticFunction.sigma 1) n) > c * ↑n ∧ ∀ (m : StrictCoveringSystem ℤ), ∃ i, ↑n ∉ m.moduli i

number theorycovering systemsN/A2 sources

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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science