Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×source:erdos-problems ×Clear all

Problem ledger

604 problems · 1/13NumberSourcesGraph view
declared open · formalized · $500erdos:1
∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), Erdos1.IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N
number theoryadditive combinatoricsA2766612 sources
declared open · formalized · $5000erdos:3
True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k
number theoryadditive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources
declared openerdos:5
Erdős problem 5
number theoryprimesA001223
declared open · formalizederdos:9
1 ∈ Erdos9.Erdos9A
number theoryadditive basisprimesA0062862 sources
declared open · formalizederdos:10
True ↔ ∃ k, Erdos10.sumPrimeAndTwoPows k = Set.univ \ {0, 1}
number theoryadditive basisprimesA3870532 sources
declared open · formalizederdos:11
∀ (n : ℕ), Odd n → 1 < n → ∃ k l, Squarefree k ∧ n = k + 2 ^ l
number theoryadditive basisA001220 · A3775873 sources
declared open · formalizederdos:12
Let A⊂NA \subset \mathbb{N} be infinite with no distinct a,b,c∈Aa, b, c \in A such that a∣(b+c)a \mid (b + c) with b,c>ab, c > a. Can ∣A∩[1,N]∣/N|A \cap [1, N]|/\sqrt{N} have positive lower limit? Must every such AA fall below N1−cN^{1-c} infinitely often?
number theoryN/A4 sources
declared open · formalizederdos:14
True ↔ ∀ (A : Set ℕ), ∀ ε > 0, Erdos14.almostSquareRoot ε =O[Filter.atTop] Erdos14.nonUniqueSumCount A
number theorysidon setsadditive combinatoricsA143824 · possible2 sources
declared open · formalizederdos:15
True ↔ Summable fun k => (-1) ^ (k + 1) * (↑k + 1) / ↑(Nat.nth Nat.Prime k)
number theoryprimesN/A2 sources
declared open · formalizederdos:17
sorry ↔ {p | Erdos17.IsClusterPrime p}.Infinite
number theoryprimesA0381332 sources
declared open · formalizederdos:18
∀ᶠ (n : ℕ) in Filter.atTop, Erdos18.practicalH n.factorial < n
number theorydivisorsfactorialsA0051532 sources
declared open · formalized · $1000erdos:20
sorry ↔ ∃ c, ∀ (n k : ℕ), n > 0 → Erdos20.f n k < c k ^ n
combinatoricsA3320772 sources
declared open · formalizederdos:25
True ↔ ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ (i : ℕ), 0 < seq_n i) → StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d
number theoryN/A3 sources
declared open · formalized · $500erdos:28
∀ (A : Set ℕ), (A + A)ᶜ.Finite → Filter.limsup (fun n => ↑(AdditiveCombinatorics.sumRep A n)) Filter.atTop = ⊤
number theoryadditive basisN/A2 sources
declared open · formalized · $1000erdos:30
True ↔ ∀ ε > 0, (fun N => ↑(Erdos30.h N) - √↑N) =O[Filter.atTop] fun N => ↑N ^ ε
number theorysidon setsadditive combinatoricsA143824 · A227590 · A0030222 sources
declared open · formalizederdos:32
True ↔ ∃ A, Erdos32.IsAdditiveComplementToPrimes A ∧ (fun N => ↑{x ∈ Finset.Icc 1 N | x ∈ A}.card) =o[Filter.atTop] fun N => Real.log ↑N ^ 2
number theoryadditive basisN/A2 sources
declared open · formalizederdos:33
⨅ A, Filter.limsup (fun N => ↑(↑A ∩ Set.Icc 1 N).ncard / ↑√↑N) Filter.atTop = sorry
number theoryadditive basisN/A2 sources
declared open · formalizederdos:36
Erdos36.M 5 = 3
number theoryadditive combinatoricsA393584 · possible3 sources
declared open · formalized · $500erdos:39
True ↔ ∃ A, A.Infinite ∧ IsSidon A ∧ ∀ ε > 0, (fun x => ↑x ^ (1 / 2 - ε)) =O[Filter.atTop] fun N => ↑(Set.Icc 1 N ∩ A).ncard
number theorysidon setsadditive combinatoricsN/A2 sources
declared open · formalized · $500erdos:40
Erdos40.Erdos40ForSet sorry
number theoryadditive basisN/A2 sources
declared open · formalized · $500erdos:41
∀ (A : Set ℕ), Erdos41.NtupleCondition A 3 → A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0
number theorysidon setsadditive combinatoricsN/A2 sources
declared open · formalizederdos:44
True ↔ ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon ↑A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (↑A ∪ ↑B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card
number theorysidon setsadditive combinatoricsN/A2 sources
declared open · formalized · $250erdos:50
sorry ↔ ∀ (f : ℝ → ℝ), Erdos50.IsDistributionOfPhiRatio f → ¬∃ x ∈ Set.Icc 0 1, ∃ y > 0, HasDerivWithinAt f y (Set.Icc 0 1) x
number theoryN/A2 sources
declared open · formalizederdos:51
True ↔ ∃ A n, A.Infinite ∧ (∀ (a : ↑A), IsLeast (Nat.totient ⁻¹' {↑a}) (n a)) ∧ Filter.Tendsto (fun a => ↑(n a) / ↑↑a) Filter.atTop Filter.atTop
number theoryA002202 · A0141973 sources
declared open · formalized · $250erdos:52
True ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ C, 0 < C ∧ ∀ (A : Finset ℤ), max ↑(A + A).card ↑(A * A).card ≥ C * ↑A.card ^ (2 - ε)
number theoryadditive combinatoricsA2639963 sources
declared open · formalizederdos:60
∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj], SimpleGraph.extremalNumber n (SimpleGraph.cycleGraph 4) < G.edgeFinset.card → c * √↑n ≤ ↑{H' | Nonempty (H'.coe ≃g SimpleGraph.cycleGraph 4)}.ncard
graph theorycyclesA0068552 sources
declared open · formalizederdos:61
sorry ↔ ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (H : SimpleGraph α), ∃ c > 0, Erdos61.IsErdosHajnalLowerBound H fun n => ↑n ^ c
graph theoryN/A2 sources
declared openerdos:62
Erdős problem 62
graph theoryN/A
declared openerdos:65
Erdős problem 65
graph theorycyclesN/A
declared open · formalized · $500erdos:66
True ↔ ∃ A c, c ≠ 0 ∧ Filter.Tendsto (fun n => ↑(AdditiveCombinatorics.sumRep A n) / Real.log ↑n) Filter.atTop (nhds c)
number theoryadditive basisN/A2 sources
declared open · formalizederdos:68
True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1))
number theoryirrationalityA3313732 sources
declared open · formalizederdos:70
True ↔ ∀ (β : Ordinal.{0}) (n : ℕ), β.card ≤ Cardinal.aleph0 → 2 ≤ n → Erdos70.OrdinalCardinalRamsey3 Cardinal.continuum.ord β ↑n
graph theoryramsey theoryset theoryN/A2 sources
declared open · formalized · $500erdos:74
∀ {V : Type u} {G : SimpleGraph V} (A : G.Subgraph), (Erdos74.SimpleGraph.edgeDistancesToBipartite A).Nonempty
graph theorychromatic numbercyclesN/A2 sources
declared open · formalizederdos:75
True ↔ ∃ V G, G.chromaticCardinal = Cardinal.aleph 1 ∧ Cardinal.mk V = Cardinal.aleph 1 ∧ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph), H.verts.ncard = n → ∃ I, ↑I ⊆ H.verts ∧ G.IsIndepSet ↑I ∧ ↑I.card > ↑n ^ (1 - ε)
graph theorychromatic numberN/A3 sources
declared open · $250erdos:77
Erdős problem 77
graph theoryramsey theoryA059442
declared open · $100erdos:78
Erdős problem 78
graph theoryramsey theoryA0594422 sources
declared openerdos:80
Erdős problem 80
graph theoryramsey theoryN/A
declared openerdos:81
Erdős problem 81
graph theorypossible2 sources
declared open · formalizederdos:82
Filter.Tendsto (fun n => ↑(Erdos82.F n) / Real.log ↑n) Filter.atTop Filter.atTop
graph theoryA120414 · A390256 · A390257 · A390919 · A392636 · A394400 · A394462 · A394539 · A394563 · A394564 · A394573 · A394574 · A394930 · A3949332 sources
declared openerdos:84
Erdős problem 84
graph theorycyclespossible
declared open · formalizederdos:85
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos85.f n ≤ Erdos85.f (n + 1)
graph theoryA006672 · possible2 sources
declared open · $100erdos:86
Erdős problem 86
graph theoryA245762
declared openerdos:87
Erdős problem 87
graph theoryramsey theoryA059442 · possible
declared open · formalized · $500erdos:89
(fun n => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)
geometrydistancesA186704 · A1316282 sources
declared open · formalizederdos:91
(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ True
geometrydistancesA186704 · possible3 sources
declared open · formalizederdos:96
∀ (n : ℕ), BddAbove (Erdos96.convexUnitDistanceCounts n)
geometrydistancesconvexpossible2 sources
declared open · formalizederdos:98
True ↔ Filter.Tendsto (fun n => ↑(Erdos98.h n) / ↑n) Filter.atTop Filter.atTop
geometrydistancespossible2 sources
declared open · formalized · $100erdos:99
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos99.HasMinDist1 A → IsMinOn (fun B => Metric.diam ↑B) {B | B.card = n ∧ Erdos99.HasMinDist1 B} A → ∃ p ∈ A, ∃ q ∈ A, ∃ r ∈ A, Erdos99.FormsEquilateralTriangle p q r
geometrydistancesN/A2 sources
declared open · formalizederdos:100
True ↔ ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → Erdos100.DistancesSeparated A → Metric.diam ↑A > C * ↑n
geometrydistancesN/A2 sources
declared open · formalized · $100erdos:101
(fun n => ↑(Erdos101.numLinesWithFourPointMax n)) =o[Filter.atTop] fun n => ↑n ^ 2
geometryA006065 · possible2 sources

Search problems.science

Find a Problem, Result, source, or page