Vela Mathematics Program: problems

Narrowed toformalized ×source:formal-conjectures ×Clear all

Problem ledger

604 problems · 10/13Number SourcesGraph view

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

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

number theorydivisorsA046801 · possible3 sources

declared disproved (Lean) · formalizederdos:897

False ↔ ∀ (f : ℕ → ℝ), (∀ a > 0, ∀ b > 0, a.Coprime b → f (a * b) = f a + f b) → Filter.limsup (fun x => match x with | (p, k) => ↑(f (p ^ k)) / ↑(Real.log (↑p ^ k))) (Filter.atTop ⊓ Filter.principal {(p, k) | Nat.Prime p}) = ⊤ → Filter.limsup (fun n => (↑(f (n + 1)) - ↑(f n)) / ↑(Real.log ↑n)) Filter.atTop = ⊤

number theoryN/A6 sources

declared proved (Lean) · formalizederdos:898

∀ (A B C P L M N : EuclideanSpace ℝ (Fin 2)), AffineIndependent ℝ ![A, B, C] → P ∈ interior ((convexHull ℝ) {A, B, C}) → N ∈ affineSpan ℝ {A, B} → (affineSpan ℝ {P, N}).direction ⟂ (affineSpan ℝ {A, B}).direction → M ∈ affineSpan ℝ {B, C} → (affineSpan ℝ {P, M}).direction ⟂ (affineSpan ℝ {B, C}).direction → L ∈ affineSpan ℝ {C, A} → (affineSpan ℝ {P, L}).direction ⟂ (affineSpan ℝ {C, A}).direction → dist P A + dist P B + dist P C ≥ 2 * (dist P M + dist P N + dist P L)

geometryN/A5 sources

declared proved · formalizederdos:899

True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N) Filter.atTop (nhds 0) → Filter.limsup (fun N => ↑((A - A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop = ⊤

additive combinatoricsN/A2 sources

declared proved (Lean) · formalizederdos:904

True ↔ ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], ∀ r ∈ Set.Icc 1 (Erdos904.n V), Erdos904.turanNumber (Erdos904.n V) r ≤ G.edgeFinset.card → ∃ s, G.IsNClique r s ∧ 2 * r * G.edgeFinset.card ≤ Erdos904.n V * ∑ v ∈ s, G.degree v

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:905

∀ (n : ℕ) (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj], ↑n ^ 2 / 4 < ↑G.edgeFinset.card → ∃ e ∈ G.edgeFinset, ↑n / 6 ≤ ↑(G.trianglesContaining e).card

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

True ↔ ∀ (f : ℝ → ℝ), (∀ (h : ℝ), 0 < h → Continuous fun x => f (x + h) - f x) → ∃ g a, Continuous g ∧ (∀ (x y : ℝ), a (x + y) = a x + a y) ∧ f = g + a

analysisN/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 proved (Lean) · formalizederdos:914

∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], Fintype.card V = r * m → m * (r - 1) ≤ G.minDegree → ∃ K, (∀ (i : Fin m), G.IsNClique r (K i)) ∧ Pairwise fun i j => Disjoint (K i) (K j)

graph theoryN/A5 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 solved · formalizederdos:920

True ↔ ∀ k ≥ 4, ∃ c > 0, (fun n => ↑n ^ (1 - 1 / (↑k - 1)) / Real.log ↑n ^ c) =O[Filter.atTop] fun n => ↑(Erdos920.f k n)

graph theorychromatic numberpossible2 sources

declared proved (Lean) · formalizederdos:923

True ↔ ∀ (V : Type u_1) (n : ℕ), ∃ k, ∀ (G : SimpleGraph V), ↑k ≤ G.chromaticNumber → ∃ H ≤ G, ↑n ≤ H.chromaticNumber ∧ H.CliqueFree 3

graph theorychromatic numberN/A5 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 proved · formalizederdos:937

True ↔ {p | Erdos937.IsCoprimePowerfulAP4 p.1 p.2}.Infinite

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

declared open · formalizederdos:945

True ↔ Erdos945.Erdos945Prop

number theorydivisorspossible · A0488922 sources

declared proved · formalizederdos:946

{n | (ArithmeticFunction.sigma 0) n = (ArithmeticFunction.sigma 0) (n + 1)}.Infinite

number theorydivisorsA005237 · A2847832 sources

declared open · formalizederdos:949

True ↔ ∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, Cardinal.mk ↑A = Cardinal.continuum ∧ A + A ⊆ Sᶜ

ramsey theoryN/A3 sources

declared open · formalizederdos:950

True ↔ Filter.liminf (fun n => ↑(Erdos950.f n)) Filter.atTop = 1

number theoryprimesN/A2 sources

declared open · formalizederdos:951

sorry ↔ ∀ (a : ℕ → ℝ), 1 < a 0 → StrictMono a → Erdos951.Erdos951Prop a → ∀ᶠ (x : ℝ) in Filter.atTop, {i | a i ≤ x}.ncard ≤ ⌊x⌋₊.primeCounting

number theoryN/A3 sources

declared open · formalizederdos:952

∃ x C, Function.Injective x ∧ ∀ (n : ℕ), Prime (x n) ∧ Zsqrtd.norm (x (n + 1) - x n) < C

number theoryN/A2 sources

declared open · formalizederdos:955

True ↔ ∀ (A : Set ℕ), A.HasDensity 0 → {x | Erdos955.s x ∈ A}.HasDensity 0

number theorypossible2 sources

declared disproved (Lean) · formalizederdos:958

False ↔ ∀ (n : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → (EuclideanGeometry.distanceSet A).card = n - 1 ∧ Finset.image (EuclideanGeometry.distanceMultiplicity A) (EuclideanGeometry.distanceSet A) = Finset.Icc 1 (n - 1) → Erdos958.IsEquidistantOnLine A ∨ Erdos958.IsEquidistantOnCircle A

distancesgeometryN/A5 sources

declared open · formalizederdos:959

How large can the difference between the largest and second-largest distance multiplicities be among

n

planar points?

geometrydistancesN/A4 sources

declared open · formalizederdos:961

True ↔ ∃ C, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos961.f k) < Real.log ↑k ^ C

number theoryA2132532 sources

declared open · formalizederdos:962

True ↔ ∃ ε, (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(Erdos962.k n) ≤ (Real.log ↑n).rpow (1 / 2 + ε n)

number theoryA3279092 sources

declared disproved · formalizederdos:965

False ↔ ∀ (f : ℝ → Fin 2), ∃ A, ¬A.Countable ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a ≠ b → c ≠ d → f (a + b) = f (c + d)

ramsey theoryN/A2 sources

declared proved (Lean) · formalizederdos:966

Let

k,r\geq 2

. Does there exist a set

A\subseteq \mathbb{N}

that contains no non-trivial arithmetic progression of length

k+1

, yet in any

r

-colouring of

A

there must exist a monochromatic non-trivial arithmetic progression of length

k

? Answered in the affirmative.

number theoryadditive combinatoricsramsey theoryN/A6 sources

declared disproved (Lean) · formalizederdos:967

False ↔ ∀ (a : ℕ → ℕ), StrictMono a → 1 < a 0 → (Summable fun k => 1 / ↑(a k)) → ∀ (t : ℝ), 1 + ∑' (k : ℕ), Erdos967.summand t (a k) ≠ 0

number theoryanalysisN/A5 sources

declared open · formalizederdos:968

sorry ↔ 0 < {n | Erdos968.u n < Erdos968.u (n + 1)}.lowerDensity

number theoryA3875912 sources

declared open · formalizederdos:971

True ↔ ∃ c > 0, ∃ C > 0, ∀ᶠ (d : ℕ) in Filter.atTop, C * ↑d.totient ≤ ↑{a ∈ Finset.Iio d | a.Coprime d ∧ ↑(Erdos971.leastCongruentPrime a d) > (1 + c) * ↑d.totient * Real.log ↑d}.card

number theoryA2265212 sources

declared open · formalizederdos:972

True ↔ ∀ α > 1, Irrational α → (Erdos972.primeSet α).Infinite

number theoryN/A2 sources

declared open · formalizederdos:973

True ↔ ∃ C > 1, ∀ n ≥ 2, ∃ z, z 1 = 1 ∧ (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) ∧ ∀ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ < C ^ (-↑n)

analysisN/A2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science