Skip to content

Problems · Vela Mathematics Program

Narrowed tosolved (Lean) ×source:jayyhk-erdos-lean ×Clear all

Problem ledger

23 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)erdos:192
Erdős problem 192
arithmetic progressionscombinatoricsN/A3 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:419
{x | MapClusterPt x Filter.atTop Erdos419.factorialDivisorRatio} = Erdos419.limitPointSet
number theoryfactorialsN/A5 sources
declared solved (Lean) · formalizederdos:459
∀ {u : ℕ}, 2 ≤ u → u + 2 ≤ Erdos459.f u ∧ Erdos459.f u ≤ u ^ 2
number theoryprimesA2892805 sources
declared solved (Lean) · formalizederdos:497
∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(DedekindNumber.M' n) = 2 ^ ((1 + o n) * ↑(n.choose (n / 2)))
combinatoricsA0003725 sources
declared solved (Lean) · formalizederdos:502
∀ (n : ℕ) (A : Set (EuclideanSpace ℝ (Fin n))), A.Finite → {d | ∃ x ∈ A, ∃ y ∈ A, x ≠ y ∧ dist x y = d}.ncard = 2 → A.ncard ≤ (n + 2).choose 2
geometrydistancesA0276275 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:648
(fun n => ↑(Erdos648.g n)) =Θ[Filter.atTop] fun n => √(↑n / Real.log ↑n)
number theoryA3917505 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)erdos:765
Erdős problem 765
graph theoryturan numberA0068553 sources
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 solved (Lean) · formalizederdos:1007
IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} sorry
graph theoryN/A5 sources
declared solved (Lean) · formalizederdos:1023
True ↔ ∃ c, 0 < c ∧ Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos1023.F n)) fun n => c * 2 ^ n / ↑n ^ (1 / 2)
combinatoricsA347025 · possible5 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:1028
(fun n => ↑(Erdos1028.H n)) =Θ[Filter.atTop] fun n => ↑n ^ (3 / 2)
graph theorydiscrepancypossible5 sources
declared solved (Lean) · formalizederdos:1044
IsGLB {L | ∃ f, Erdos1044.IsAdmissible f ∧ Erdos1044.maxBoundaryLength f = L} 2
analysisN/A5 sources
declared solved (Lean) · formalizederdos:1102
∀ (A : ℕ → ℕ), StrictMono A → Erdos1102.HasPropertyP (Set.range A) → Filter.Tendsto (fun j => ↑(A j) / ↑j) Filter.atTop Filter.atTop
number theoryN/A5 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
declared solved (Lean) · formalizederdos:1193
False ↔ ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0
additive combinatoricsN/A5 sources

Search problems.science

Find a Problem, Result, source, or page