Vela Mathematics Program: problems

Problem ledger

319 problems · 5/7Number SourcesGraph view

declared open · formalizederdos:726

True ↔ Asymptotics.IsEquivalent Filter.atTop (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n => Real.log (Real.log ↑n) / 2

number theoryN/A3 sources

declared open · formalizederdos:727

True ↔ ∀ k ≥ 2, {n | (n + k).factorial ^ 2 ∣ (2 * n).factorial}.Infinite

number theoryfactorialsA002503 · A343507 · A3893962 sources

declared open · formalizederdos:730

True ↔ Erdos730.S.Infinite

number theorybinomial coefficientsbase representationsA1295154 sources

declared open · formalizederdos:740

True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 ≤ G.chromaticCardinal → ∀ (r : ℕ), ∃ H, H.coe.chromaticCardinal = G.chromaticCardinal ∧ Erdos740.NoShortOddCycle H.coe r

graph theorychromatic numberN/A2 sources

declared open · formalizederdos:749

True ↔ ∀ ε > 0, ∃ A, 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun n => 1

additive combinatoricsN/A3 sources

declared open · formalizederdos:757

∀ {A : Set ℝ}, sorry = sSup {c | Erdos757.IsAdmissible c}

geometrydistancessidon setspossible2 sources

declared open · formalizederdos:769

For the least cutoff

c(n)

after which every

k

occurs as the number of homothetic cubes in a decomposition of the unit

n

-cube, is

c(n) \gg n^n

? The Lean proof shows

c(n) = o(n^n)

along odd dimensions.

number theorygeometryA014544 · possible4 sources

declared open · formalizederdos:770

∀ {n : ℕ}, 2 < n → (Erdos770.h n = ↑n + 1 ↔ Nat.Prime (n + 1))

number theoryA263647 · possible2 sources

declared open · formalizederdos:774

True ↔ ∀ (A : Set ℕ), A.Infinite → A.IsProportionatelyDissociated → ∃ T, (∀ S ∈ T, S.IsDissociated) ∧ T.Finite ∧ A = ⋃₀ T

number theoryN/A2 sources

declared open · formalizederdos:786

Erdos786.consecutivePrimesFrom 2 1 = {2, 3}

number theoryA143301 · possible2 sources

declared open · formalizederdos:789

(fun n => ↑(Erdos789.subsetSumThreshold n)) =Θ[Filter.atTop] sorry

additive combinatoricspossible2 sources

declared open · formalizederdos:796

g_3(n)

is the largest size of

A \subseteq [1,n]

with fewer than three representations of every product

a_1 a_2

, does its conjectured second-order normalized term converge? The candidate proof gives an explicit limit constant.

number theorypossible5 sources

declared open · formalizederdos:812

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) / ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 1 + c

graph theoryramsey theoryA0594422 sources

declared open · formalizederdos:817

True ↔ (fun n => 3 ^ n) =O[Filter.atTop] fun n => ↑(Erdos817.g 3 n)

additive combinatoricspossible2 sources

declared open · formalizederdos:821

True ↔ ∀ ε > 0, {n | ↑(Erdos821.g n) > ↑n ^ (1 - ε)}.Infinite

number theoryA0141972 sources

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

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

number theoryprimesA001223 · A3907692 sources

declared open · formalizederdos:855

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

number theoryprimesA0231932 sources

declared open · formalizederdos:857

have f := sorry; ∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun n => ↑(Erdos857.m n k) / f k n) Filter.atTop (nhds 1)

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

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

number theorydivisorsA046801 · possible3 sources

declared open · formalizederdos:906

Is there an entire non-zero function

f:\mathbb{C}\to \mathbb{C}

such that, for any infinite sequence

n_1<n_2<\cdots

, the set

\{ z: f^{(n_k)}(z)=0 \textrm{ for some }k\geq 1\}

is everywhere dense? The literal question is trivial for polynomials, so the claims address the transcendental entire case, in the affirmative.

analysisiterated functionsN/A5 sources

declared open · formalizederdos:912

∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => c * (↑n / Real.log ↑n) ^ (1 / 2)

number theoryfactorialsA0716262 sources

declared open · formalizederdos:913

True ↔ {n | Set.InjOn ⇑(n * (n + 1)).factorization ↑(n * (n + 1)).primeFactors}.Infinite

number theoryA3597472 sources

declared open · formalizederdos:918

True ↔ ∃ V G, Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph 1 → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0

graph theorychromatic numberN/A2 sources

declared open · formalizederdos:930

True ↔ ∀ r > 0, ∃ k, ∀ (I₁ I₂ : Fin r → ℕ), (∀ (i : Fin r), 0 < I₁ i ∧ I₁ i + k ≤ I₂ i + 1) → (∀ (i j : Fin r), i < j → I₂ i < I₁ j) → ¬Erdos930.IsPower (∏ i, ∏ m ∈ Finset.Icc (I₁ i) (I₂ i), m)

number theoryN/A2 sources

declared open · formalizederdos:931

sorry ↔ ∀ (k₁ k₂ : ℕ), k₂ ≥ 3 → k₂ ≤ k₁ → {(n₁, n₂) | n₁ + k₁ ≤ n₂ ∧ (∏ i ∈ Finset.Icc 1 k₁, (n₁ + i)).primeFactors = (∏ j ∈ Finset.Icc 1 k₂, (n₂ + j)).primeFactors}.Finite

number theoryN/A3 sources

declared open · formalizederdos:932

{r | 2 ≤ {m ∈ Finset.Ioo (Nat.nth Nat.Prime r) (Nat.nth Nat.Prime r.succ) | m.maxPrimeFac < Nat.nth Nat.Prime r.succ - Nat.nth Nat.Prime r}.card}.Infinite

number theoryA3878642 sources

declared open · formalizederdos:933

True ↔ Filter.limsup (fun n => ↑↑(2 ^ Erdos933.k n * 3 ^ Erdos933.l n) / (↑↑n * ↑(Real.log ↑n))) Filter.atTop = ⊤

number theorypossible2 sources

declared open · formalizederdos:936

True ↔ Erdos936.EventuallyNotPowerful fun x => x.factorial + 1

number theoryA146968 · possible2 sources

declared open · formalizederdos:938

True ↔ {P | (↑P).IsAPOfLength 3 ∧ ∃ k, P = {Nat.nth Nat.Powerful k, Nat.nth Nat.Powerful (k + 1), Nat.nth Nat.Powerful (k + 2)}}.Finite

number theoryA001694 · A076446 · possible2 sources

declared open · formalizederdos:939

True ↔ ∀ r ≥ 4, (Erdos939.Erdos939Sums r).Nonempty

number theorypossible2 sources

declared open · formalizederdos:940

True ↔ ∀ r ≥ 3, {n | ∃ S, S.card ≤ r ∧ (∀ s ∈ S, r.Full s) ∧ n = S.sum}.HasDensity 0

number theorypossible2 sources

declared open · formalizederdos:942

Let

h(n)

count powerful integers in

[n^2, (n+1)^2)

. What is the extremal order of

h(n)

number theorypossible4 sources

declared open · formalizederdos:943

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(AdditiveCombinatorics.sumRep Nat.Powerful n) ≤ ↑n ^ o n

number theorypossible4 sources

declared open · formalizederdos:944

True ↔ ∀ k ≥ 4, ∀ r ≥ 1, ∃ V G, Erdos944.SimpleGraph.IsErdos944 G k r

graph theorychromatic numberN/A2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science