Vela Mathematics Program: problems

Narrowed toformalized ×source:formal-conjectures ×Clear all

Problem ledger

604 problems · 2/13Number SourcesGraph view

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 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 disproved (Lean) · formalized · $500erdos:90

Conjectured upper bound on how many pairs among

n

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 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

declared open · formalized · $100erdos:101

(fun n => ↑(Erdos101.numLinesWithFourPointMax n)) =o[Filter.atTop] fun n => ↑n ^ 2

geometryA006065 · possible2 sources

declared disproved (Lean) · formalized · $50erdos:105

False ↔ ∀ (A B : Finset (EuclideanSpace ℝ (Fin 2))), Disjoint A B → A.card = B.card + 3 → ¬Collinear ℝ ↑A → ∃ p ∈ A, ∃ q ∈ A, p ≠ q ∧ ∀ b ∈ B, b ∉ affineSpan ℝ {p, q}

geometryN/A5 sources

declared falsifiable · formalized · $500erdos:107

sorry ↔ ∀ n ≥ 3, Erdos107.f n = 2 ^ (n - 2) + 1

geometryconvexA0000512 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 proved · formalizederdos:109

∀ (A : Set ℕ), A.upperDensity > 0 → ∃ B C, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

additive combinatoricsN/A2 sources

declared proved (Lean) · formalizederdos:115

True ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (p : Polynomial ℂ), p.Monic → p.natDegree = n → IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} → ∀ (z : ℂ), ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 2

polynomialsanalysisN/A5 sources

declared solved · formalized · $100erdos:119

For unit-modulus complex numbers

z_i

, let

p_n(z)=\prod_{i\le n}(z-z_i)

and

M_n=\max_{|z|=1}|p_n(z)|

. Erdős's prize question: is there

c>0

with

\sum_{k\le n} M_k > n^{1+c}

analysispolynomialsN/A4 sources

declared open · formalized · $100erdos:120

True ↔ ∀ (A : Set ℝ), A.Infinite → Erdos120.Erdos120For A

combinatoricsN/A3 sources

declared proved (Lean) · formalized · $250erdos:123

Let

a,b,c>1

be pairwise coprime integers. Is every large integer a sum of distinct numbers of the form

a^k b^l c^m

(

k,l,m\ge 0

), none dividing another?

number theoryN/A5 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 disproved (Lean) · formalizederdos:125

False ↔ ({x | (Nat.digits 3 x).toFinset ⊆ {0, 1}} + {x | (Nat.digits 4 x).toFinset ⊆ {0, 1}}).HasPosDensity

number theorybase representationsA3670906 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 falsifiable · formalized · $250erdos:128

True ↔ ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), (∀ (V' : Set V), 2 * V'.ncard + 1 ≥ Fintype.card V → 50 * (SimpleGraph.induce V' G).edgeSet.ncard > Fintype.card V ^ 2) → ¬G.CliqueFree 3

graph theoryN/A2 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 proved (Lean) · formalizederdos:134

True ↔ ∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∃ N, ∀ n ≥ N, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 3 → (∀ (v : Fin n), ↑(G.degree v) < (↑n).rpow (1 / 2 - ε)) → ∃ H, G ≤ H ∧ H.CliqueFree 3 ∧ (∀ (x y : Fin n), x ≠ y → H.Adj x y ∨ ∃ z, H.Adj x z ∧ H.Adj z y) ∧ ↑(H.edgeFinset \ G.edgeFinset).card ≤ δ * ↑n ^ 2

graph theoryN/A5 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

W(k)

is the least

N

such that every two-colouring of

\{1, \dots, N\}

contains a monochromatic

k

-term arithmetic progression, must

W(k+1) - W(k) \to \infty

additive combinatoricsA0053464 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 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

declared open · formalizederdos:145

True ↔ ∀ α ≥ 0, ∃ β, Filter.Tendsto (fun x => 1 / x * ∑ n ∈ Erdos145.A x, (↑(Erdos145.s (n + 1)) - ↑(Erdos145.s n)) ^ α) Filter.atTop (nhds β)

number theoryA0051172 sources

declared open (Lean) · formalized · $500erdos:146

H

is bipartite and

r

-degenerate, is

\mathrm{ex}(n;H) \ll n^{2-1/r}

(a $500 Erdős-Simonovits prize conjecture)? A counterexample refutes the degeneracy conjecture.

graph theoryturan numberN/A3 sources

declared proved (Lean) · formalizederdos:150

True ↔ ∃ α < 2, Filter.Tendsto (fun n => ↑(Erdos150.maxMinimalCuts n) ^ (1 / ↑n)) Filter.atTop (nhds α)

graph theorypossible5 sources

declared proved · formalizederdos:152

True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop

sidon setsN/A4 sources

declared open · formalizederdos:153

True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop

sidon setsN/A2 sources

declared proved (Lean) · formalizederdos:154

True ↔ ∀ (m : ℕ), 2 ≤ m → ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ), Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop → (∀ (k x : ℕ), x ∈ A k → x ≤ N k) → (∀ (k : ℕ), IsSidon ↑(A k)) → Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) → ∀ i < m, Filter.Tendsto (fun k => ↑{s ∈ A k + A k | s % m = i}.card / ↑(A k + A k).card) Filter.atTop (nhds (1 / ↑m))

sidon setsN/A6 sources

declared open · formalizederdos:155

True ↔ ∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, Erdos155.F (N + k) ≤ Erdos155.F N + 1

additive combinatoricssidon setsA143824 · A227590 · A0030222 sources

declared open · formalizederdos:156

True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)

sidon setsA3823972 sources

declared open · formalizederdos:158

∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon A

sidon setsN/A2 sources

declared open · formalizederdos:160

have lower_bound := sorry; (lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧ ∀ c > 0, ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) → ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound

additive combinatoricsarithmetic progressionspossible2 sources

declared proved (Lean) · formalizederdos:164

True ↔ ∀ (A : Set ℕ), (∀ a ∈ A, 2 ≤ a) → Erdos1196.IsPrimitive A → ∑' (a : ↑A), 1 / (↑↑a * Real.log ↑↑a) ≤ ∑' (p : ↑{p | Nat.Prime p}), 1 / (↑↑p * Real.log ↑↑p)

number theoryprimitive setsA1372455 sources

declared open · formalizederdos:168

Erdos168.F 0 = 0

additive combinatoricsA004059 · A057561 · A094708 · A3864392 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science