Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 9/12Number SourcesGraph view

declared open · formalizederdos:826

True ↔ ∃ C > 0, {n | ∀ k ≥ 1, ↑((ArithmeticFunction.sigma 0) (n + k)) ≤ C * ↑k}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:828

True ↔ ∀ (a : ℤ), {n | ↑n.totient ∣ ↑n + a}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:829

True ↔ ∃ C, (fun n => ↑(AdditiveCombinatorics.sumRep Erdos829.cubes n)) =O[Filter.atTop] fun n => Real.log ↑n ^ C

number theorypossible2 sources

declared open · formalizederdos:830

sorry ↔ {(a, b) | IsAmicable a b}.Infinite

number theoryA2591802 sources

declared openerdos:839

Erdős problem 839

number theoryN/A

declared solvederdos:841

Erdős problem 841

number theoryA092487

declared provederdos:843

Erdős problem 843

number theoryN/A

declared proved (Lean) · formalizederdos:844

True ↔ ∀ (N : ℕ), IsGreatest {k | ∃ A ⊆ Finset.Icc 1 N, (∀ a ∈ A, ∀ b ∈ A, ¬Squarefree (a * b)) ∧ A.card = k} (Erdos844.evenOrOddNonSquarefree N).card

number theoryintersecting familyN/A5 sources

declared disproved (Lean) · formalizederdos:845

False ↔ ∀ (C : ℝ), 0 < C → have f := fun x => match x with | (k, l) => 2 ^ k * 3 ^ l; {x | ∃ B, ∃ (h : B.Nonempty) (_ : ↑(B.sup f) ≤ C * ↑(B.inf' h f)), ∑ x ∈ B, f x = x}.HasDensity 0

number theoryN/A5 sources

declared decidable · formalizederdos:848

Is the maximum size of a set

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

such that

ab+1

is never squarefree (for all

a,b\in A

) achieved by taking those

n\equiv 7\pmod{25}

? Resolved for all sufficiently large

N

: any near-maximal

A

is contained in

\{n\equiv 7\pmod{25}\}

\{n\equiv 18\pmod{25}\}

, leaving only a finite check.

number theoryN/A4 sources

declared open · formalizederdos:849

True ↔ ∀ t ≥ 1, ∃ a, {n | ∃ k ≥ 1, 2 * k ≤ n ∧ n.choose k = a}.ncard = t

number theorybinomial coefficientsA003016 · A003015 · A059233 · A098565 · A090162 · A180058 · A1822372 sources

declared open · formalizederdos:850

True ↔ ∃ x y, x ≠ y ∧ x.primeFactors = y.primeFactors ∧ (x + 1).primeFactors = (y + 1).primeFactors ∧ (x + 2).primeFactors = (y + 2).primeFactors

number theoryprimesA3431013 sources

declared proved · formalizederdos:851

∀ ε ∈ Set.Ioo 0 1, ∃ r d, (Erdos851.TwoPowAddSet r).HasDensity d ∧ 1 - ε ≤ d

number theoryN/A4 sources

declared openerdos:852

Erdős problem 852

number theoryprimesA001223 · A053597 · A0785152 sources

declared open · formalizederdos:853

Filter.Tendsto Erdos853.r Filter.atTop Filter.atTop

number theoryprimesA001223 · A3907692 sources

declared openerdos:854

Erdős problem 854

number theoryA389839 · A048670

declared open · formalizederdos:855

True ↔ ∀ᶠ (x : ℕ) (y : ℕ) in Filter.atTop, (x + y).primeCounting ≤ x.primeCounting + y.primeCounting

number theoryprimesA0231932 sources

declared openerdos:856

Let

k\geq 3

and

f_k(N)

be the maximum of

\sum_{n\in A}\frac{1}{n}

over all

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

containing no

k

subsets with the same pairwise least common multiple. Estimate

f_k(N)

. The claimed answer:

f_k(N)=(\log N)^{\gamma_k+o(1)}

, where

\gamma_k

is a weighted generalization of the Tang-Zhang sunflower capacity.

number theorypossible3 sources

declared solvederdos:858

Erdős problem 858

number theoryprimitive setsN/A4 sources

declared open · formalizederdos:859

∃ c₁ > 0, ∃ c₂ > 0, ∃ d, (∀ t > 0, (Erdos859.DivisorSumSet t).HasDensity (d t)) ∧ Asymptotics.IsEquivalent Filter.atTop (fun t => d t) fun t => c₁ / Real.log ↑t ^ c₂

number theorydivisorsN/A2 sources

declared openerdos:860

Erdős problem 860

number theoryprimesA048670 · A058989

declared solvederdos:861

Erdős problem 861

number theorysidon setsA143824 · A227590 · A003022 · A143823

declared solved (Lean) · formalizederdos:862

False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)

number theorysidon setsA3823955 sources

declared provederdos:863

Erdős problem 863

number theorysidon setsadditive combinatoricsN/A3 sources

declared openerdos:864

Erdős problem 864

number theorysidon setsadditive combinatoricsA3891822 sources

declared proved (Lean) · formalizederdos:865

∃ C > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ 5 / 8 * ↑N + C → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A

number theoryadditive combinatoricspossible5 sources

declared openerdos:866

Estimate the least excess

g_k(N)

forcing

k

integers whose pairwise sums all lie in a dense subset of

\{1, \dots, 2N\}

; in particular, determine the positive variant

h_4(n)

number theoryadditive combinatoricspossible5 sources

declared solved · formalizederdos:868

False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 → Filter.Tendsto (fun n => Erdos868.ncard_add_repr A 2 n) Filter.atTop Filter.atTop → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2

number theoryadditive basisN/A3 sources

declared disprovederdos:869

Erdős problem 869

number theoryadditive basisN/A

declared openerdos:870

Let

k\geq 3

and

A

be an additive basis of order

k

. Does there exist a constant

c=c(k)>0

such that if

r(n)\geq c\log n

for all large

n

(where

r(n)

counts representations of

n

as a sum of at most

k

elements of

A

) then

A

must contain a minimal basis of order

k

? The claimed answer is no, for every

k\geq 3

number theoryadditive basisN/A3 sources

declared disproved (Lean) · formalizederdos:871

False ↔ ∀ (A : Set ℕ), ((∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧ ∀ (t : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ pairs, pairs.card ≥ t ∧ ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) → ∃ B C, (∀ (x : ℕ), x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧ Disjoint B C ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n

number theoryadditive basisN/A6 sources

declared open · formalizederdos:872

True ↔ ∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos872.L n) ≥ ε * ↑n

number theoryprimitive setspossible3 sources

declared open · formalizederdos:873

True ↔ ∀ (a : ℕ → ℕ), ∀ ε > 0, 0 < a 0 → StrictMono a → ∃ k, ∀ X > 0, ↑↑(Erdos873.F a X k) < ↑(X ^ ε)

number theoryN/A3 sources

declared provederdos:874

Erdős problem 874

number theoryadditive combinatoricspossible

declared openerdos:878

Erdős problem 878

number theoryA339378 · possible

declared openerdos:879

Erdős problem 879

number theoryA186736

declared provederdos:880

Erdős problem 880

number theoryadditive basisN/A

declared open · formalizederdos:881

True ↔ ∀ (k : ℕ) (A : Set ℕ), Erdos881.IsMinimalAsymptoticAddBasisOfOrder k A → ∃ B ⊆ A, B.Infinite ∧ (A \ B).IsAsymptoticAddBasisOfOrder (k + 1)

number theoryadditive basisN/A2 sources

declared solvederdos:882

Erdős problem 882

number theoryprimitive setspossible

declared openerdos:883

Erdős problem 883

number theorygraph theoryN/A

declared disproved (Lean) · formalizederdos:884

False ↔ Erdos884.Erdos884Prop

number theorydivisorsN/A3 sources

declared open · formalizederdos:885

True ↔ ∀ k ≥ 1, ∃ Ns, (∀ n ∈ Ns, 1 ≤ n) ∧ Ns.card = k ∧ (⋂ n ∈ Ns, Erdos885.factorDifferenceSet n).ncard ≥ k

number theorydivisorsN/A2 sources

declared open · formalizederdos:886

sorry ↔ ∀ ε > 0, ∃ K, ∀ᶠ (n : ℕ) in Filter.atTop, (Erdos886.Erdos886Divisors n ε 1).card ≤ K

number theorydivisorsN/A2 sources

declared open · formalizederdos:887

∀ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, {d ∈ Finset.Ioo ⌊√↑n⌋₊ ⌈√↑n + C * ↑n ^ (1 / 4)⌉₊ | d ∣ n}.card ≤ sorry

number theorydivisorsN/A2 sources

declared solved · formalizederdos:888

(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n

number theorysquaresA3875845 sources

declared open · formalizederdos:889

Filter.Tendsto Erdos889.v₀ Filter.atTop (nhds ⊤)

number theorypossible2 sources

declared open · formalizederdos:890

sorry ↔ ∀ k ≥ 1, Filter.liminf (fun n => ∑ i ∈ Finset.range k, ↑(Erdos890.omegaGt k (n + i))) Filter.atTop ≤ ↑k

number theoryprimesN/A2 sources

declared open · formalizederdos:891

True ↔ ∀ k ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ m ∈ Finset.Ico n (n + ∏ i ∈ Finset.range k, Nat.nth Nat.Prime i), k < ArithmeticFunction.cardDistinctFactors m

number theoryN/A2 sources

declared openerdos:892

Erdős problem 892

number theoryprimitive setsN/A

declared open · formalizederdos:893

True ↔ Filter.Tendsto (fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n)) Filter.atTop Filter.atTop

number theorydivisorsA046801 · possible3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science