Vela Mathematics Program: problems

Problem ledger

114 problems · 1/3Number SourcesGraph view

declared proved (Lean) · formalizederdos:45

True ↔ ∀ (k : ℕ), 2 ≤ k → ∃ n, ∀ (colouring : ℕ → Fin k), ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1

number theoryunit fractionsramsey theorypossible4 sources

declared proved (Lean) · formalizederdos:46

True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ (𝓒 '' ↑S).Subsingleton

number theoryunit fractionsramsey theoryN/A4 sources

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

Erdős problem 87

graph theoryramsey theoryA059442 · possible

declared proved · $100erdos:88

Erdős problem 88

graph theoryramsey theoryN/A

declared openerdos:112

Erdős problem 112

graph theoryramsey theorypossible

declared disprovederdos:118

Erdős problem 118

set theoryramsey theoryN/A

declared openerdos:129

Erdős problem 129

graph theoryramsey theorypossible

declared openerdos:159

Erdős problem 159

graph theoryramsey theorypossible

declared open · $500erdos:161

Erdős problem 161

combinatoricsramsey theorydiscrepancyN/A2 sources

declared openerdos:162

Erdős problem 162

combinatoricsramsey theorydiscrepancyN/A

declared provederdos:163

Erdős problem 163

graph theoryramsey theoryN/A

declared open · $250erdos:165

Erdős problem 165

graph theoryramsey theoryA0007912 sources

declared proved · $250erdos:166

Erdős problem 166

graph theoryramsey theoryA059442

declared open · formalizederdos:172

True ↔ ∀ (n : ℕ) (color : ℕ → Fin n) (m : ℕ), ∃ A, A.card ≥ m ∧ ∃ c, ∀ (S : Finset ↥A), S.Nonempty → color (∑ x ∈ S, ↑x) = c ∧ color (∏ x ∈ S, ↑x) = c

additive combinatoricsramsey theoryN/A2 sources

declared openerdos:173

Erdős problem 173

geometryramsey theoryN/A

declared openerdos:174

Erdős problem 174

geometryramsey theoryN/A

declared openerdos:181

Erdős problem 181

graph theoryramsey theorypossible

declared open (Lean) · formalized · $250erdos:183

Let

R(3;k)

be the least

n

such that every

k

-colouring of the edges of

K_n

contains a monochromatic triangle. Determine

\lim_{k\to\infty} R(3;k)^{1/k}

(a $250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

graph theoryramsey theoryA0033233 sources

declared openerdos:187

Erdős problem 187

additive combinatoricsramsey theoryN/A

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 sources

declared disproved (Lean) · formalizederdos:189

False ↔ Erdos189.Erdos189For (fun a b c d => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun a b c d => dist a b * dist b c

geometryramsey theoryN/A5 sources

declared provederdos:191

Erdős problem 191

combinatoricsramsey theoryN/A

declared provederdos:439

Erdős problem 439

number theoryramsey theoryN/A

declared not provable · $100erdos:474

Erdős problem 474

set theoryramsey theoryN/A

declared openerdos:483

Erdős problem 483

number theoryadditive combinatoricsramsey theoryA030126

declared proved (Lean) · formalizederdos:484

∃ c, 0 < c ∧ ∀ (k : ℕ), 0 < k → ∃ N₀, ∀ (N : ℕ), N₀ ≤ N → ∀ (f : ℕ → Fin k), c * ↑N ≤ ↑{n ∈ Finset.Icc 1 N | ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n}.card

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared open · formalizederdos:508

4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber

geometryramsey theoryN/A2 sources

declared provederdos:518

Erdős problem 518

graph theoryramsey theoryN/A

declared openerdos:531

Erdős problem 531

number theoryramsey theorypossible

declared proved (Lean) · formalizederdos:532

True ↔ ∀ (c : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∃ color, ∀ (S : Finset ℕ), S.Nonempty → ↑S ⊆ A → c (∑ n ∈ S, n) = color

number theoryramsey theoryN/A4 sources

declared openerdos:544

Erdős problem 544

graph theoryramsey theoryA000791

declared openerdos:545

Erdős problem 545

graph theoryramsey theoryA059442 · possible

declared provederdos:546

Erdős problem 546

graph theoryramsey theorypossible

declared decidableerdos:547

Erdős problem 547

graph theoryramsey theoryN/A

declared disprovederdos:549

Erdős problem 549

graph theoryramsey theoryN/A

declared openerdos:550

Let

m_1\leq\cdots\leq m_k

and

n

be sufficiently large. If

T

is a tree on

n

vertices and

G

is the complete multipartite graph with vertex class sizes

m_1,\ldots,m_k

, prove that

R(T,G)\leq (\chi(G)-1)(R(T,K_{m_1,m_2})-1)+m_1

graph theoryramsey theoryN/A4 sources

declared decidableerdos:551

Erdős problem 551

graph theoryramsey theoryN/A

declared openerdos:552

Erdős problem 552

graph theoryramsey theoryA006672

declared provederdos:553

Erdős problem 553

graph theoryramsey theoryA000791 · possible

declared openerdos:554

Erdős problem 554

graph theoryramsey theorypossible

declared openerdos:555

Erdős problem 555

graph theoryramsey theoryA389313 · possible

declared decidableerdos:556

Erdős problem 556

graph theoryramsey theoryA389335

Problems · Vela Mathematics Program

Problem ledger

Search problems.science