Vela Mathematics Program: problems

Problem ledger

319 problems · 2/7Number SourcesGraph view

declared open · formalizederdos:145

True ↔ ∀ α ≥ 0, ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)

number theoryA0051172 sources

declared open · formalizederdos:153

True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop

sidon setsN/A2 sources

declared open · formalizederdos:155

True ↔ ∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, Erdos155.F (N + k) ≤ Erdos155.F N + 1

additive combinatoricssidon setsA143824 · A227590 · A0030222 sources

declared open · formalizederdos:156

True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)

sidon setsA3823972 sources

declared open · formalizederdos:158

∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon A

sidon setsN/A2 sources

declared open · formalizederdos:160

have lower_bound := sorry; (lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧ ∀ c > 0, ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) → ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound

additive combinatoricsarithmetic progressionspossible2 sources

declared open · formalizederdos:168

Erdos168.F 0 = 0

additive combinatoricsA004059 · A057561 · A094708 · A3864392 sources

declared open · formalizederdos:170

Filter.Tendsto (fun N => ↑(Erdos170.F N) / √↑N) Filter.atTop (nhds sorry)

additive combinatoricsA0466932 sources

declared open · formalizederdos:172

True ↔ ∀ (n : ℕ) (color : ℕ → Fin n) (m : ℕ), ∃ A, A.card ≥ m ∧ ∃ c, ∀ (S : Finset ↥A), S.Nonempty → color (∑ x ∈ S, ↑x) = c ∧ color (∏ x ∈ S, ↑x) = c

additive combinatoricsramsey theoryN/A2 sources

declared open · formalizederdos:184

∃ f, (f =O[Filter.atTop] fun n => ↑n) ∧ ∀ {V : Type u_1} [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V), ∃ D, (∀ H ∈ D, Erdos184.IsCycleOrEdge H.coe) ∧ Erdos184.IsDecomposition G D ∧ ↑D.card ≤ f (Fintype.card V)

graph theorycyclespossible2 sources

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 sources

declared open · formalizederdos:193

True ↔ ∀ (S : Set (Fin 3 → ℤ)), S.Finite → ∀ (a : ℕ → Fin 3 → ℤ), Erdos193.IsSWalk S a → (Set.range a).Infinite → Erdos193.HasCollinearTriple ℚ (Set.range fun n => Int.cast ∘ a n)

geometryA2312552 sources

declared open · formalizederdos:195

sorry = sSup {k | ∀ (f : ℤ ≃ ℤ), HasMonotoneAP (⇑f) k}

arithmetic progressionsN/A2 sources

declared open · formalizederdos:196

True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4

arithmetic progressionsN/A2 sources

declared open · formalizederdos:197

True ↔ ∃ A B, IsCompl A B ∧ (∃ f, ¬HasMonotoneAP (Subtype.val ∘ ⇑f) 3) ∧ ∃ g, ¬HasMonotoneAP (Subtype.val ∘ ⇑g) 3

arithmetic progressionsN/A2 sources

declared open · formalizederdos:200

sorry ↔ (fun n => ↑(Erdos200.longestPrimeArithmeticProgressions n)) =o[Filter.atTop] fun n => Real.log ↑n

primesarithmetic progressionsA0051152 sources

declared open · formalizederdos:203

True ↔ ∃ m, m.Coprime 6 ∧ ∀ (k l : ℕ), ¬Nat.Prime (2 ^ k * 3 ^ l * m + 1)

primescovering systemsN/A2 sources

declared open · formalizederdos:208

True ↔ ∀ ε > 0, (fun n => ↑(Erdos208.erdos208.s (n + 1)) - ↑(Erdos208.erdos208.s n)) =O[Filter.atTop] fun n => ↑(Erdos208.erdos208.s n) ^ ε

number theoryA005117 · A0762592 sources

declared open · formalizederdos:212

True ↔ ∃ u, Dense u ∧ u.Pairwise fun c₁ c₂ => dist c₁ c₂ ∈ Set.range Rat.cast

geometrydistancesN/A2 sources

declared open · formalizederdos:213

True ↔ ∀ n ≥ 4, Erdos213.Erdos213For n

geometrydistancesN/A2 sources

declared open · formalizederdos:218

{n | primeGap (n + 1) ≤ primeGap n}.HasDensity (1 / 2)

number theoryprimesA333230 · A333231 · A0641133 sources

declared open · formalizederdos:233

(fun N => ∑ n ∈ Finset.range N, ↑(primeGap n) ^ 2) =O[Filter.atTop] fun N => ↑N * Real.log ↑N ^ 2

number theoryprimesA0747413 sources

declared open · formalizederdos:234

True ↔ ∃ f, Continuous f ∧ ∀ (c : NNReal), {n | ↑(primeGap n) / Real.log ↑n < ↑c}.HasDensity (f c)

number theoryprimesN/A2 sources

declared open · formalizederdos:236

(fun n => ↑(Erdos236.f n)) =o[Filter.atTop] fun n => Real.log ↑n

number theoryprimesA039669 · A1099252 sources

declared open · formalizederdos:238

True ↔ ∀ c₁ > 0, ∀ c₂ > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∃ k, c₁ * Real.log x < ↑k ∧ ∃ f m, (∀ (i : Fin k), ↑(f i) ≤ x ∧ f i = Nat.nth Nat.Prime (m + ↑i)) ∧ ∀ (i : Fin (k - 1)), c₂ < primeGap (m + ↑i)

number theoryprimesN/A2 sources

declared open · formalized · $100erdos:241

True ↔ Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos241.f N 3)) fun N => ↑N ^ (1 / 3)

additive combinatoricssidon setsA3877042 sources

declared open · formalizederdos:243

∀ (a : ℕ → ℕ), StrictMono a → Filter.Tendsto (fun n => ↑(a n) / ↑(a (n - 1)) ^ 2) Filter.atTop (nhds 1) → (Summable fun x => 1 / ↑(a x)) → ∀ᶠ (n : ℕ) in Filter.atTop, a n = a (n - 1) ^ 2 - a (n - 1) + 1

number theoryA0000582 sources

declared open · formalizederdos:244

True ↔ ∀ C > 1, 0 < {x | ∃ p k, ∃ (_ : Nat.Prime p), p + ⌊C ^ k⌋₊ = x}.lowerDensity

number theoryprimesN/A2 sources

declared open · formalizederdos:247

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → Filter.limsup (fun k => ↑(n k) / ↑k.succ) Filter.atTop = ⊤ → Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)

number theoryirrationalityN/A2 sources

declared open · formalizederdos:249

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

number theoryirrationalityA2569362 sources

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 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 open · formalizederdos:257

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

irrationalityN/A2 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 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 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 open · formalizederdos:269

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

irrationalityN/A2 sources

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 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 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 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 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 open · formalizederdos:291

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

number theoryunit fractionsA1105663 sources

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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science