Skip to content

Problems · Vela Mathematics Program

Narrowed tosource:erdos-problems ×Clear all

Problem ledger

1,217 problems · 2/25NumberSourcesGraph view
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 provederdos:53
Erdős problem 53
number theoryadditive combinatoricspossible
declared solved · $100erdos:54
Erdős problem 54
number theoryramsey theoryN/A
declared solved · $250erdos:55
Erdős problem 55
number theoryramsey theoryN/A
declared disproved (Lean) · formalized · $10erdos:56
∀ {A : Finset ℕ}, Erdos56.WeaklyDivisible 0 A ↔ A = ∅
number theoryintersecting familyN/A5 sources
declared provederdos:57
Erdős problem 57
graph theorychromatic numbercyclesN/A
declared provederdos:58
Erdős problem 58
graph theorychromatic numbercyclesN/A
declared disprovederdos:59
Erdős problem 59
graph theoryturan numberN/A
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 provederdos:63
Erdős problem 63
graph theorychromatic numbercyclesN/A
declared falsifiable · formalized · $1000erdos:64
True ↔ ∀ (V : Type u_1) (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.minDegree ≥ 3 → ∃ k v c, k ≥ 2 ∧ c.IsCycle ∧ c.length = 2 ^ k
graph theorycyclesN/A2 sources
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 proved · formalized · $500erdos:67
∀ (f : ℕ → ↥{-1, 1}) (C : ℝ), 0 < C → ∃ d ≥ 1, ∃ m ≥ 1, C < |∑ k ∈ Finset.Icc 1 m, ↑(f (k * d))|
discrepancyA181740 · A2376952 sources
declared open · formalizederdos:68
True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1))
number theoryirrationalityA3313732 sources
declared proved · formalizederdos:69
Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2))
number theoryirrationalityA2621532 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 proved (Lean) · formalizederdos:71
True ↔ ∀ (P : Set ℕ), P.IsAPOfLength ⊤ → (∃ n ∈ P, Even n) → ∃ c, ∀ (V : Type) [inst : Fintype V] [DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj], c ≤ G.averageDegree → ∃ v w, w.IsCycle ∧ w.length ∈ P
graph theorycyclesN/A4 sources
declared proved · $100erdos:72
Erdős problem 72
graph theorycyclesN/A
declared provederdos:73
Erdős problem 73
graph theoryN/A
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 provederdos:76
Erdős problem 76
graph theoryramsey theoryA060407
declared open · $250erdos:77
Erdős problem 77
graph theoryramsey theoryA059442
declared open · $100erdos:78
Erdős problem 78
graph theoryramsey theoryA0594422 sources
declared provederdos:79
Erdős problem 79
graph theoryramsey theoryN/A
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 proved · $500erdos:83
Erdős problem 83
combinatoricsA071799 · A387635
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 proved · $100erdos:88
Erdős problem 88
graph theoryramsey theoryN/A
declared open · formalized · $500erdos:89
(fun n => ↑n / √(Real.log ↑n)) =O[Filter.atTop] fun n => ↑(EuclideanGeometry.minimalDistinctDistances n)
geometrydistancesA186704 · A1316282 sources
declared disproved (Lean) · formalized · $500erdos:90
Conjectured upper bound on how many pairs among nn points in the plane can be exactly one unit apart.
geometrydistancesA1867055 sources
declared open · formalizederdos:91
(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ True
geometrydistancesA186704 · possible3 sources
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 proved (Lean) · formalizederdos:93
∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.ConvexIndep ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A
geometryconvexdistancesN/A5 sources
declared proved (Lean) · formalized · £25erdos:94
∃ C > 0, ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.ConvexIndep ↑P → ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤ C * ↑P.card ^ 3
geometryconvexdistancesA3878585 sources
declared proved · $500erdos:95
Erdős problem 95
geometryconvexdistancespossible
declared open · formalizederdos:96
∀ (n : ℕ), BddAbove (Erdos96.convexUnitDistanceCounts n)
geometrydistancesconvexpossible2 sources
declared falsifiable · formalized · $100erdos:97
True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.ConvexIndep ↑A → ¬Erdos97.HasNEquidistantProperty 4 A
geometrydistancesconvexN/A2 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

Search problems.science

Find a Problem, Result, source, or page