Skip to content

Problems · Vela Mathematics Program

Narrowed tosource:gpt-erdos ×Clear all

Problem ledger

57 problems · 2/2NumberSourcesGraph view
declared proved (Lean) · formalizederdos:1022
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)
combinatoricshypergraphspossible6 sources
declared open · formalizederdos:1063
have upper_bound := sorry; (fun k => ↑(Erdos1063.n k)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun k => ↑k * (Finset.Icc 1 (k - 1)).lcm fun n => ↑n
number theoryA3893603 sources
declared open · formalizederdos:1084
∀ {n : ℕ}, n ≠ 0 → Erdos1084.f 2 n < 3 * n
geometrydistancesA045945 · possible3 sources
declared disproved · formalizederdos:1092
False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)
geometrychromatic numberN/A5 sources
declared proved · formalizederdos:1105
True ↔ ∀ (k : ℕ), 3 ≤ k → (fun n => ↑((SimpleGraph.cycleGraph k).antiRamseyNum n) - ((↑k - 2) / 2 + 1 / (↑k - 1)) * ↑n) =O[Filter.atTop] fun x => 1
graph theoryramsey theorypossible3 sources
declared provederdos:1129
Erdős problem 1129
analysispolynomialsN/A2 sources
declared provederdos:1130
Erdős problem 1130
analysispolynomialsN/A2 sources