Skip to content

Problems · Vela Mathematics Program

Narrowed tosolved (Lean) ×source:vibemathed ×Clear all

Problem ledger

9 problemsGraph view
declared solved (Lean) · formalizederdos:42
True ↔ ∀ M ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}
number theorysidon setsadditive combinatoricsN/A6 sources
declared solved (Lean) · formalizederdos:202
∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos202.f N) = ↑N * scaleL N ^ (-1 + o N)
covering systemsA3899756 sources
declared solved (Lean) · formalizederdos:619
False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(Erdos619.minNewEdges 4 G) < (1 - c) * ↑(Fintype.card V)
graph theoryN/A5 sources
declared solved (Lean) · formalizederdos:650
∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊
number theoryA0274346 sources
declared solved (Lean) · formalizederdos:694
∀ (fmax fmin : ℕ → ℕ), (∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) → (∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) → ∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ ∀ (x : ℕ), sSup {x_1 | ∃ n, ∃ (_ : n ≤ x) (_ : ∃ m, m.totient = n), ↑(fmax n) / ↑(fmin n) = x_1} = (Real.exp Real.eulerMascheroniConstant + o x) * Real.log (Real.log ↑x)
number theorypossible6 sources
declared solved (Lean)erdos:696
Erdős problem 696
number theorydivisorspossible4 sources
declared solved (Lean) · formalizederdos:741
True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity
additive combinatoricsN/A6 sources
declared solved (Lean) · formalizederdos:1026
For a sequence of nn distinct reals, determine the largest constant cc such that some monotonic subsequence always has sum exceeding (c−o(1))⋅(1/n)(c-o(1))\cdot(1/\sqrt{n}) times the total sum. Resolved as c=1c = 1.
combinatoricsA391431 · A3914906 sources
declared solved (Lean) · formalizederdos:1190
∀ (ε : ℝ), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps m ∧ Erdos1190.eps m < scaleL m ^ (-1 + ε)
number theorycovering systemspossible6 sources

Search problems.science

Find a Problem, Result, source, or page