Vela Mathematics Program: problems

Narrowed todisproved ×source:erdos-problems ×Clear all

Problem ledger

69 problems · 1/2Number SourcesGraph view

declared disproved · $1000erdos:2

Erdős problem 2

number theorycovering systemsA160559

declared disprovederdos:8

Erdős problem 8

number theorycovering systemsN/A

declared disproved · $100erdos:27

Erdős problem 27

number theorycovering systemsN/A

declared disprovederdos:37

Erdős problem 37

number theoryadditive combinatoricsN/A

declared disproved · formalized · $100erdos:43

If Sidon sets

A, B \subseteq \{1, \dots, N\}

satisfy

(A-A) \cap (B-B) = \{0\}

, must

\binom{|A|}{2} + \binom{|B|}{2} \le \binom{f(N)}{2} + O(1)

, where

f(N)

is the largest Sidon-set size in

[N]

- and can the bound be improved by a fixed proportion when

|A| = |B|

number theorysidon setsadditive combinatoricsA143824 · A227590 · A003022 · possible4 sources

declared disprovederdos:59

Erdős problem 59

graph theoryturan numberN/A

declared disproved · formalized · $500erdos:92

sorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos92.f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))

geometrydistancespossible2 sources

declared disprovederdos:110

Erdős problem 110

graph theorychromatic numbercyclesN/A

declared disproved · $500erdos:113

Erdős problem 113

graph theoryturan numberN/A

declared disprovederdos:118

Erdős problem 118

set theoryramsey theoryN/A

declared disprovederdos:121

Erdős problem 121

number theorysquaresA028391 · A013928 · A372306 · A373319 · A372306 · A373178 · A360659 · A373114 · A143301

declared disprovederdos:133

Erdős problem 133

graph theorypossible

declared disproved · $250erdos:135

Erdős problem 135

distancesgeometrypossible

declared disproved · $500erdos:147

Erdős problem 147

graph theoryturan numberN/A

declared disprovederdos:216

Erdős problem 216

geometryconvexA381776

declared disprovederdos:227

Erdős problem 227

analysisN/A

declared disprovederdos:230

Erdős problem 230

analysispolynomialsN/A

declared disproved · formalizederdos:253

¬∀ (a : ℕ → ℕ), 0 < a 0 → Erdos253.RepresentsAPs a → Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 1) → subsetSums (Set.range a) ∈ Filter.cofinite

number theoryN/A2 sources

declared disproved · formalizederdos:266

¬∀ (a : ℕ → ℕ), ((∀ (n : ℕ), a n ≥ 1) ∧ Summable fun x => 1 / ↑(a x)) → ∃ t ≥ 1, Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑t))

irrationalityN/A2 sources

declared disprovederdos:270

Erdős problem 270

irrationalityA073016

declared disprovederdos:309

Erdős problem 309

number theoryunit fractionsA217693

declared disprovederdos:381

Erdős problem 381

number theorydivisorsA002182

declared disprovederdos:441

Erdős problem 441

number theoryA0685092 sources

declared disproved · formalizederdos:442

False ↔ ∀ (A : Set ℕ), Filter.Tendsto (fun x => 1 / Erdos442.Real.maxLogOne (Erdos442.Real.maxLogOne x) * ∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) Filter.atTop Filter.atTop → Filter.Tendsto (fun x => 1 / (∑ n ∈ (A ∩ Set.Icc 1 ⌊x⌋₊).toFinset, 1 / ↑n) ^ 2 * ∑ nm ∈ (Erdos442.Set.bddProdUpper A x).toFinset, 1 / ↑(nm.1.lcm nm.2)) Filter.atTop Filter.atTop

number theoryN/A2 sources

declared disproved · formalizederdos:448

False ↔ ∀ (ε : ℝ), 0 < ε → {n | ↑(Erdos448.tauPlus n) < ε * ↑n.divisors.card}.HasDensity 1

number theorydivisorsA3974332 sources

declared disprovederdos:449

Erdős problem 449

number theorydivisorspossible

declared disprovederdos:492

Erdős problem 492

number theoryN/A

declared disprovederdos:511

Erdős problem 511

analysisN/A

declared disproved · formalizederdos:533

False ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 5 → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ∃ S, c * ↑n ≤ ↑S.card ∧ G.CliqueFreeOn (↑S) 3

graph theoryN/A3 sources

declared disprovederdos:543

Erdős problem 543

number theorygroup theorypossible3 sources

declared disprovederdos:549

Erdős problem 549

graph theoryramsey theoryN/A

declared disprovederdos:559

Erdős problem 559

graph theoryramsey theorypossible

declared disprovederdos:574

Erdős problem 574

graph theoryturan numberpossible

declared disprovederdos:586

Erdős problem 586

number theorycovering systemsN/A

declared disproved · formalizederdos:615

False ↔ ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum

graph theoryramsey theorypossible2 sources

declared disprovederdos:632

Erdős problem 632

graph theorychromatic numberN/A

declared disprovederdos:641

Erdős problem 641

graph theoryN/A

declared disprovederdos:651

Erdős problem 651

geometryconvexpossible

declared disprovederdos:664

Erdős problem 664

combinatoricsN/A

declared disproved · formalizederdos:705

False ↔ ∃ k, ∀ (V : Set (EuclideanSpace ℝ (Fin 2))), V.Finite → (SimpleGraph.UnitDistancePlaneGraph V).girth ≥ k → (SimpleGraph.UnitDistancePlaneGraph V).chromaticNumber ≤ 3

graph theorychromatic numberN/A3 sources

declared disprovederdos:744

Erdős problem 744

graph theorychromatic numberpossible

declared disprovederdos:763

Erdős problem 763

number theoryadditive combinatoricsN/A

declared disprovederdos:764

Erdős problem 764

number theoryadditive combinatoricsN/A

declared disprovederdos:781

Erdős problem 781

additive combinatoricspossible

declared disprovederdos:803

Erdős problem 803

graph theoryN/A

declared disprovederdos:804

Erdős problem 804

graph theorypossible

declared disprovederdos:807

Erdős problem 807

graph theoryN/A

declared disprovederdos:808

Erdős problem 808

additive combinatoricsgraph theoryN/A

declared disprovederdos:815

Erdős problem 815

graph theoryN/A

declared disprovederdos:832

Erdős problem 832

graph theoryhypergraphschromatic numberpossible

Problems · Vela Mathematics Program

Problem ledger

Search problems.science