Vela Mathematics Program: problems

Narrowed toproved (Lean) ×number theory ×Clear all

Problem ledger

66 problems · 1/2Number SourcesGraph view

declared proved (Lean) · formalizederdos:31

∀ (A : Set ℕ), A.Infinite → ∃ B, B.HasDensity 0 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, n ∈ A + B

declared proved (Lean) · formalizederdos:38

True ↔ ∃ B, ¬B.IsWeakAddBasis ∧ ∃ f, (∀ (α : ℝ), 0 < α → α < 1 → f α > 0) ∧ ∀ (A : Set ℕ) (N : ℕ), have α := schnirelmannDensity A; ∃ b ∈ B, ↑(Set.Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * ↑N

number theoryN/A6 sources

declared proved (Lean) · formalizederdos:45

True ↔ ∀ (k : ℕ), 2 ≤ k → ∃ n, ∀ (colouring : ℕ → Fin k), ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1

number theoryunit fractionsramsey theorypossible4 sources

declared proved (Lean) · formalizederdos:46

True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ (𝓒 '' ↑S).Subsingleton

number theoryunit fractionsramsey theoryN/A4 sources

declared proved (Lean) · formalized · $100erdos:47

True ↔ ∀ (δ : ℝ), 0 < δ → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, δ * Real.log ↑N < A.reciprocalSum → ∃ S ⊆ A, S.reciprocalSum = 1

number theoryunit fractionsN/A4 sources

declared proved (Lean) · formalized · $250erdos:123

Let

a,b,c>1

be pairwise coprime integers. Is every large integer a sum of distinct numbers of the form

a^k b^l c^m

(

k,l,m\ge 0

), none dividing another?

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:164

True ↔ ∀ (A : Set ℕ), (∀ a ∈ A, 2 ≤ a) → Erdos1196.IsPrimitive A → ∑' (a : ↑A), 1 / (↑↑a * Real.log ↑↑a) ≤ ∑' (p : ↑{p | Nat.Prime p}), 1 / (↑↑p * Real.log ↑↑p)

number theoryprimitive setsA1372455 sources

declared proved (Lean) · formalizederdos:221

True ↔ ∃ A, ((fun N => ↑{a | a ∈ A ∧ a ≤ N}.ncard) =O[Filter.atTop] fun N => ↑N / Real.log ↑N) ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∃ k a, 0 ≤ k ∧ a ∈ A ∧ N = 2 ^ k + a

number theoryadditive basisN/A5 sources

declared proved (Lean)erdos:237

Erdős problem 237

number theoryprimesN/A4 sources

declared proved (Lean) · formalizederdos:246

∀ (a b : ℕ), 2 ≤ a → 2 ≤ b → a.Coprime b → IsAddComplete (Erdos246.Gamma a b)

number theoryN/A5 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 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 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 proved (Lean) · formalizederdos:283

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

number theoryunit fractionsA3807916 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 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 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 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 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 proved (Lean) · formalizederdos:330

True ↔ ∃ A h, Erdos330.MinAsymptoticAddBasisOfOrder A h ∧ 0 < A.upperDensity ∧ ∀ n ∈ A, 0 < (Erdos330.UnrepWithout A n h).upperDensity

number theoryadditive basisN/A5 sources

declared proved (Lean) · formalizederdos:347

True ↔ ∃ a, Monotone a ∧ Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 2) ∧ ∀ (ι : ℕ → ℕ), (Set.range ι)ᶜ.Finite → (subsetSums (Set.range (a ∘ ι))).HasDensity 1

number theorycomplete sequencesN/A6 sources

declared proved (Lean) · formalizederdos:350

∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (A : Finset M), Erdos350.DistinctSubsetSums ↑A ↔ Erdos350.DecidableDistinctSubsetSums A

number theoryadditive combinatoricsN/A5 sources

declared proved (Lean) · formalizederdos:351

True ↔ ∀ (P : Polynomial ℚ), 0 < P.natDegree → 0 < P.leadingCoeff → Erdos351.HasCompleteImage P

number theorycomplete sequencesN/A6 sources

declared proved (Lean) · formalizederdos:355

True ↔ ∃ A, IsLacunary A ∧ ∃ u v, u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x | ∃ A', ∃ (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}

number theoryunit fractionsN/A5 sources

declared proved (Lean) · formalizederdos:369

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ (k : ℕ), 2 ≤ k → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε

number theoryN/A7 sources

declared proved (Lean) · formalizederdos:370

True ↔ {n | ↑n.maxPrimeFac < √↑n ∧ ↑(n + 1).maxPrimeFac < √(↑n + 1)}.Infinite

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:379

Filter.limsup (fun n => ↑(Erdos379.S n)) Filter.atTop = ⊤

number theorybinomial coefficientspossible5 sources

declared proved (Lean) · formalizederdos:392

∀ (A : ℕ → ℕ), (∀ n > 0, IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n ^ 2), t + 1 = x} (A n)) → (fun n => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

number theoryfactorialspossible5 sources

declared proved (Lean) · formalizederdos:401

True ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (r : ℕ), 1 ≤ r → {n | ∃ a₁ a₂, 0 < a₁ ∧ 0 < a₂ ∧ ↑a₁ + ↑a₂ > ↑n + f r * Real.log ↑n ∧ a₁.factorial * a₂.factorial ∣ n.factorial * (∏ i ∈ Finset.range r, Nat.nth Nat.Prime i) ^ n}.Infinite

number theoryfactorialsN/A6 sources

declared proved (Lean) · formalizederdos:403

True ↔ {p | (∀ a ∈ p.2, 0 < a) ∧ 2 ^ p.1 = ∑ a ∈ p.2, a.factorial}.Finite

number theoryfactorialsN/A4 sources

declared proved (Lean) · formalizederdos:418

True ↔ {x | ∃ n, n - n.totient = x}ᶜ.Infinite

number theoryA005278 · A2639585 sources

declared proved (Lean) · formalizederdos:427

True ↔ Erdos427.erdos427

number theoryprimesN/A5 sources

declared proved (Lean)erdos:433

Erdős problem 433

number theorypossible4 sources

declared proved (Lean) · formalizederdos:434

∀ (n k : ℕ), 1 ≤ n → 2 ≤ k → k ≤ n → IsGreatest {x | ∃ S, ∃ (_ : S ⊆ Finset.Icc 1 n) (_ : S.card = k) (_ : S.gcd id = 1), Erdos434.Nat.NcardUnrepresentable ↑S = x} (Erdos434.Nat.NcardUnrepresentable (Set.Icc (n - k + 1) n))

number theorypossible5 sources

declared proved (Lean) · formalizederdos:435

∀ (n : ℕ), n ≠ 0 → (∀ (p k : ℕ), Nat.Prime p → n ≠ p ^ k) → IsGreatest {m | ¬∃ c, m = ∑ i ∈ Finset.Ico 1 n, ↑(c i) * ↑(n.choose i)} (∑ p ∈ n.primeFactors, (∑ d ∈ Finset.Icc 1 (n.factorization p), ↑(n.choose (p ^ d))) * (↑p - 1) - ↑n)

number theoryA3894795 sources

declared proved (Lean) · formalizederdos:443

True ↔ ∀ (s : ℕ), ∃ m, ∃ n < m, s ≤ (Erdos443.A n ∩ Erdos443.A m).card

number theoryN/A5 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 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 proved (Lean) · formalizederdos:469

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

number theorydivisorsA006036 · A119425 · possible5 sources

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 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 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 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 proved (Lean)erdos:490

Erdős problem 490

number theoryA3972054 sources

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 (Lean) · formalizederdos:532

True ↔ ∀ (c : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∃ color, ∀ (S : Finset ℕ), S.Nonempty → ↑S ⊆ A → c (∑ n ∈ S, n) = color

number theoryramsey theoryN/A4 sources

declared proved (Lean) · formalizederdos:540

True ↔ ∃ C, 0 < C ∧ ∀ (N : ℕ), 0 < N → ∀ (A : Finset (ZMod N)), C * √↑N ≤ ↑A.card → Erdos540.HasZeroSubsetSum A

number theoryA0344635 sources

declared proved (Lean) · formalizederdos:541

True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (a : Fin p → ZMod p), (∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2

number theoryN/A5 sources

declared proved (Lean) · formalizederdos:645

∀ (c : ℕ → Bool), ∃ x d, 0 < x ∧ x < d ∧ ∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C

number theoryadditive combinatoricsramsey theoryN/A5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science