Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×formalized ×source:erdos-problems ×Clear all

Problem ledger

319 problems · 1/7NumberSourcesGraph 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 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 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 · 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 open · formalizederdos:85
True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos85.f n ≤ Erdos85.f (n + 1)
graph theoryA006672 · possible2 sources
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
declared open · formalizederdos:108
True ↔ ∀ r ≥ 4, ∀ k ≥ 2, ∃ f, ∀ (V : Type u) (G : SimpleGraph V), Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k
graph theorychromatic numbercyclespossible2 sources
declared open · formalized · $100erdos:120
True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A
combinatoricsN/A3 sources
declared open · formalizederdos:124
∀ {D : Finset ℕ}, (∀ d ∈ D, 3 ≤ d) → (∀ᶠ (n : ℕ) in Filter.atTop, n ∈ ∑ d ∈ D, Erdos124.sumsOfDistinctPowers d 0) → 1 ≤ ∑ d ∈ D, (↑d - 1)⁻¹
number theorybase representationsN/A4 sources
declared open · formalized · $250erdos:126
True ↔ ∀ (f : ℕ → ℕ), Erdos126.IsMaximalAddFactorsCard f → Filter.Tendsto (fun n => ↑(f n) / Real.log ↑n) Filter.atTop Filter.atTop
number theorypossible2 sources
declared open · formalizederdos:130
For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.
graph theorychromatic numberN/A4 sources
declared open · formalizederdos:137
sorry ↔ ∀ k ≥ 3, ∀ (n : ℕ), ¬(∏ x ∈ Finset.Ioc n (n + k), x).Powerful
number theoryN/A2 sources
declared open · formalized · $500erdos:138
If W(k)W(k) is the least NN such that every two-colouring of {1,…,N}\{1, \dots, N\} contains a monochromatic kk-term arithmetic progression, must W(k+1)−W(k)→∞W(k+1) - W(k) \to \infty?
additive combinatoricsA0053464 sources
declared open · formalizederdos:141
sorry ↔ ∀ k ≥ 3, ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s k
additive combinatoricsprimesarithmetic progressionsA0065602 sources
declared open · formalized · $10000erdos:142
∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry
additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources
declared open · formalized · $500erdos:143
True ↔ ∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Filter.liminf (fun x => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0
primitive setsN/A2 sources

Search problems.science

Find a Problem, Result, source, or page