Vela Mathematics Program: problems

Problem ledger

1,217 problems · 19/25Number SourcesGraph view

declared openerdos:901

Erdős problem 901

combinatoricshypergraphspossible

declared openerdos:902

Erdős problem 902

graph theoryA362137

declared provederdos:903

Erdős problem 903

combinatoricsN/A

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 provederdos:908

Erdős problem 908

analysisN/A

declared provederdos:909

Erdős problem 909

analysistopologyN/A

declared disprovederdos:910

Erdős problem 910

topologyN/A

declared openerdos:911

Erdős problem 911

graph theoryramsey theoryN/A

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 solvederdos:915

Erdős problem 915

graph theoryN/A

declared provederdos:916

Erdős problem 916

graph theorycyclesN/A

declared openerdos:917

Erdős problem 917

graph theorychromatic numberN/A

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 openerdos:919

Erdős problem 919

graph theorychromatic numberN/A

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 provederdos:921

Erdős problem 921

graph theorychromatic numbercyclespossible

declared provederdos:922

Erdős problem 922

graph theorychromatic numberN/A

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 provederdos:924

Erdős problem 924

graph theoryramsey theoryN/A

declared disprovederdos:925

Erdős problem 925

graph theoryramsey theorypossible

declared provederdos:926

Erdős problem 926

graph theorypossible

declared disproved (Lean)erdos:927

Erdős problem 927

graph theorypossible3 sources

declared openerdos:928

Erdős problem 928

number theoryA006530

declared openerdos:929

Erdős problem 929

number theorypossible

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 openerdos:934

Erdős problem 934

graph theorypossible

declared openerdos:935

Erdős problem 935

number theoryA057521 · A389244 · possible2 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 provederdos:941

Erdős problem 941

number theoryA056828

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

Erdős problem 947

number theorycovering systemsN/A4 sources

declared solvederdos:948

Erdős problem 948

number theoryramsey theoryN/A3 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

Problems · Vela Mathematics Program

Problem ledger