Vela Mathematics Program: problems

Problem ledger

576 problems · 4/12Number SourcesGraph view

declared disproved (Lean) · formalizederdos:328

False ↔ ∀ (C : ℕ), 0 < C → ∃ t, ∀ (A : Set ℕ), (∀ (n : ℕ), AdditiveCombinatorics.sumRep A n ≤ C) → ∃ P, ⋃ i, P i = A ∧ Set.univ.PairwiseDisjoint P ∧ ∀ (i : Fin t) (n : ℕ), AdditiveCombinatorics.sumRep (P i) n < C

number theoryadditive combinatoricsN/A4 sources

declared open · formalizederdos:329

sSup {x | ∃ A, ∃ (_ : IsSidon A), Erdos329.sidonUpperDensity A = x} = sorry

number theorypossible2 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 disproved (Lean) · formalizederdos:331

False ↔ ∀ (A B : Set ℕ), ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count A n)) → ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count B n)) → {(a₁, a₂, b₁, b₂) | a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧ a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁}.Infinite

number theoryadditive combinatoricsN/A5 sources

declared open · formalizederdos:332

∀ (A : Set ℕ), sorry A → Erdos332.HasBoundedGaps (Erdos332.D_A A)

number theoryN/A3 sources

declared disproved (Lean) · formalizederdos:333

False ↔ ∀ (A : Set ℕ), A.HasDensity 0 → ∃ B, A ⊆ B + B ∧ (fun N => ↑(B ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => √↑N

number theoryadditive basisN/A6 sources

declared openerdos:334

Erdős problem 334

number theoryA062241 · A045535

declared openerdos:335

Erdős problem 335

number theoryadditive combinatoricsN/A2 sources

declared openerdos:336

h(r)

is the maximal finite exact order attainable by an additive basis of order at most

r

, what is

\lim_{r \to \infty} h(r)/r^2

? The candidate proof identifies the sharp limit

1/3

number theoryadditive basispossible2 sources

declared disproved (Lean) · formalizederdos:337

False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasis → ((fun N => ↑(A ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) → Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTop

number theoryadditive combinatoricsadditive basisN/A5 sources

declared openerdos:338

Erdős problem 338

number theoryadditive basisN/A

declared provederdos:339

Erdős problem 339

number theoryadditive basisN/A

declared open · formalizederdos:340

∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard

number theoryadditive combinatoricssidon setsA080200 · A0052822 sources

declared open · formalizederdos:341

True ↔ ∀ (a : ℕ → ℤ), (∀ᶠ (n : ℕ) in Filter.atTop, IsLeast {x | a n < x ∧ x ∉ {x | ∃ i ≤ n, ∃ j ≤ n, a i + a j = x}} (a (n + 1))) → have d := fun i => a (i + 1) - a i; ∃ p > 0, ∀ᶠ (m : ℕ) in Filter.atTop, d (m + p) = d m

number theoryN/A2 sources

declared open · formalizederdos:342

sorry ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → {n | ∃ m, a m = a n + 2}.Infinite

number theoryA0028583 sources

declared provederdos:343

Erdős problem 343

number theorycomplete sequencesN/A

declared provederdos:344

Erdős problem 344

number theorycomplete sequencesN/A

declared openerdos:345

Erdős problem 345

number theorycomplete sequencesA0016612 sources

declared open · formalizederdos:346

Let

A=\{1\leq a_1< a_2<\cdots\}

be a set of integers such that

A\backslash B

is complete for any finite subset

B

and not complete for any infinite subset

B

. If

a_{n+1}/a_n \geq 1+\epsilon

for all

n

, must

\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2

? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

number theorycomplete sequencesN/A4 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 open · formalizederdos:348

{x | ∃ m n, ∃ (_ : m < n), ∃ a, ∃ (_ : Monotone a) (_ : ∀ (s : Finset ℕ), s.card = m → IsAddComplete (Set.range (Function.updateFinset a s 0))) (_ : ∀ (t : Finset ℕ), t.card = n → ¬IsAddComplete (Set.range (Function.updateFinset a t 0))), (m, n) = x} = sorry

number theorycomplete sequencesN/A2 sources

declared open · formalizederdos:349

∀ (t α : ℝ), 0 < t → 2 < α → ¬Erdos349.IsGoodPair t α

number theorycomplete sequencesN/A3 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 open · formalizederdos:354

True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2)

number theoryN/A2 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 provederdos:356

Erdős problem 356

number theorypossible

declared open · formalizederdos:357

(fun n => ↑(Erdos357.f n)) =o[Filter.atTop] fun n => ↑n

number theoryA364132 · A364153 · possible2 sources

declared proved · formalizederdos:358

True ↔ ∃ A, StrictMono A ∧ Filter.Tendsto (Erdos358.f A) Filter.atTop Filter.atTop

number theoryadditive basisprimespossible3 sources

declared open · formalizederdos:359

∀ (A : ℕ → ℕ), Erdos359.IsGoodFor A 1 → Filter.Tendsto (fun k => ↑(A k) / ↑k) Filter.atTop Filter.atTop

number theoryA0020482 sources

declared solvederdos:360

Erdős problem 360

number theorypossible

declared open · formalizederdos:361

∀ (c : ℝ), 0 < c → Erdos361.subsetSumAvoidanceNumber c = sorry

number theorypossible2 sources

declared provederdos:362

Erdős problem 362

number theorypossible

declared disproved (Lean) · formalizederdos:363

False ↔ {S | Erdos363.IsValidCollection S}.Finite

number theoryN/A5 sources

declared verifiable · formalizederdos:364

¬∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful

number theoryA060355 · A0764452 sources

declared openerdos:365

Erdős problem 365

number theoryA060355 · A060859 · A175155

declared verifiable · formalizederdos:366

True ↔ ∃ n > 0, Nat.Full 2 n ∧ Nat.Full 3 (n + 1)

number theoryA0603553 sources

declared openerdos:367

Erdős problem 367

number theoryA0575213 sources

declared openerdos:368

Erdős problem 368

number theoryA0743993 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 open · formalizederdos:371

{n | (n + 1).maxPrimeFac > n.maxPrimeFac}.HasDensity (1 / 2)

number theoryA0700892 sources

declared provederdos:372

Erdős problem 372

number theoryA071870

declared open · formalizederdos:373

Erdos373.S.Finite

number theoryfactorialsA0031352 sources

declared openerdos:374

Erdős problem 374

number theoryA388851 · A387184 · A389117 · A3891482 sources

declared falsifiable · formalizederdos:375

True ↔ Erdos375.Erdos375Prop

number theoryN/A2 sources

declared open · formalizederdos:376

True ↔ {n | n.centralBinom.Coprime 105}.Infinite

number theorybinomial coefficientsbase representationsA0309792 sources

declared open · formalizederdos:377

True ↔ ∃ C > 0, ∀ (n : ℕ), Erdos377.sumInvPrimesNotDvdCentralBinom n ≤ C

number theorybinomial coefficientsN/A2 sources

declared provederdos:378

Erdős problem 378

number theorybinomial coefficientsN/A

declared proved (Lean) · formalizederdos:379

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

number theorybinomial coefficientspossible5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science