Skip to content

Problems · Vela Mathematics Program

Narrowed toproved ×additive combinatorics ×Clear all

Problem ledger

21 problemsGraph view
declared provederdos:53
Erdős problem 53
number theoryadditive combinatoricspossible
declared proved · formalizederdos:109
∀ (A : Set ℕ), A.upperDensity > 0 → ∃ B C, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A
additive combinatoricsN/A2 sources
declared proved · formalized · $1000erdos:139
∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)
additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources
declared proved · $500erdos:140
Erdős problem 140
additive combinatoricsarithmetic progressionsA003002
declared provederdos:171
Erdős problem 171
additive combinatoricscombinatoricsA156989
declared provederdos:179
Erdős problem 179
additive combinatoricsarithmetic progressionspossible
declared provederdos:185
Erdős problem 185
additive combinatoricsA003142
declared proved · formalizederdos:219
∅ ∉ Erdos219.primeArithmeticProgressions
number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources
declared proved · formalizederdos:245
True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0) → 3 ≤ Filter.limsup (fun N => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard) Filter.atTop
additive combinatoricsN/A2 sources
declared proved · formalizederdos:494
∀ (k card p : ℕ), Nat.Prime p → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494.Erdos494Unique k card
analysisadditive combinatoricsN/A2 sources
declared provederdos:656
Erdős problem 656
number theoryadditive combinatoricsN/A
declared provederdos:772
Erdős problem 772
number theorysidon setsadditive combinatoricspossible
declared provederdos:806
Erdős problem 806
additive combinatoricspossible
declared provederdos:863
Erdős problem 863
number theorysidon setsadditive combinatoricsN/A3 sources
declared provederdos:874
Erdős problem 874
number theoryadditive combinatoricspossible
declared provederdos:877
Erdős problem 877
additive combinatoricsA121269 · possible
declared provederdos:895
Erdős problem 895
additive combinatoricsgraph theoryN/A
declared proved · formalizederdos:899
True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N) Filter.atTop (nhds 0) → Filter.limsup (fun N => ↑((A - A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop = ⊤
additive combinatoricsN/A2 sources
declared provederdos:984
Erdős problem 984
arithmetic progressionsadditive combinatoricsN/A
declared provederdos:1179
Erdős problem 1179
additive combinatoricsprobabilityN/A
declared provederdos:1213
Erdős problem 1213
additive combinatoricspossible

Search problems.science

Find a Problem, Result, source, or page