Vela Mathematics Program: problems

Problem ledger

1,217 problems · 16/25Number SourcesGraph view

declared disproved (Lean) · formalizederdos:751

False ↔ ∀ (k : ℕ), ∃ V G, G.chromaticNumber = 4 ∧ ∀ m ∈ G.cycleLengths, ∀ m' ∈ G.cycleLengths, m < m' → m + k ≤ m'

graph theorychromatic numberN/A5 sources

declared provederdos:752

Erdős problem 752

graph theorycyclesN/A

declared disproved (Lean) · formalizederdos:753

False ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ), 0 < n → ∀ (G : SimpleGraph (Fin n)), ↑n ^ (1 / 2 + c) < ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ)

graph theorychromatic numberN/A5 sources

declared provederdos:754

Erdős problem 754

geometrydistancespossible

declared proved · formalizederdos:755

True ↔ ∃ o, (o =o[Filter.atTop] fun x => 1) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos755.TUnit 6 n) ≤ (1 / 27 + o n) * ↑n ^ 3

geometrypossible2 sources

declared proved (Lean) · formalizederdos:756

True ↔ (fun n => ↑n) =O[Filter.atTop] fun n => ↑(Erdos756.maxRichDistances n)

geometrydistancespossible5 sources

declared open · formalizederdos:757

∀ {A : Set ℝ}, sorry = sSup {c | Erdos757.IsAdmissible c}

geometrydistancessidon setspossible2 sources

declared solvederdos:758

Erdős problem 758

graph theorychromatic numberpossible

declared solvederdos:759

Erdős problem 759

graph theorychromatic numberpossible

declared proved (Lean) · formalizederdos:760

True ↔ ∃ c > 0, ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ), G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * ↑m / Real.log ↑m ≤ ↑k

graph theorychromatic numberN/A5 sources

declared openerdos:761

Erdős problem 761

graph theorychromatic numberN/A

declared disproved (Lean) · formalizederdos:762

False ↔ ∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V), G.CliqueFree 5 → 4 ≤ G.cochromaticNumber → G.chromaticNumber ≤ G.cochromaticNumber + 2

graph theorychromatic numberN/A5 sources

declared disprovederdos:763

Erdős problem 763

number theoryadditive combinatoricsN/A

declared disprovederdos:764

Erdős problem 764

number theoryadditive combinatoricsN/A

declared solved (Lean)erdos:765

Erdős problem 765

graph theoryturan numberA0068553 sources

declared openerdos:766

Erdős problem 766

graph theoryturan numberpossible

declared provederdos:767

Erdős problem 767

graph theoryturan numberpossible

declared openerdos:768

Let

A(x)

count

n \le x

such that every prime

p \mid n

has a divisor

d > 1

n

with

d \equiv 1 \pmod p

. Erdos asked whether

A(x)/x = \exp(-(c+o(1))\sqrt{\log x}\log\log x)

. It does, with

c = 1/(2\sqrt{\log 2})

number theoryA001034 · A3522873 sources

declared open · formalizederdos:769

For the least cutoff

c(n)

after which every

k

occurs as the number of homothetic cubes in a decomposition of the unit

n

-cube, is

c(n) \gg n^n

? The Lean proof shows

c(n) = o(n^n)

along odd dimensions.

number theorygeometryA014544 · possible4 sources

declared open · formalizederdos:770

∀ {n : ℕ}, 2 < n → (Erdos770.h n = ↑n + 1 ↔ Nat.Prime (n + 1))

number theoryA263647 · possible2 sources

declared provederdos:771

Erdős problem 771

number theorypossible

declared provederdos:772

Erdős problem 772

number theorysidon setsadditive combinatoricspossible

declared openerdos:773

Erdős problem 773

number theorysidon setssquaresA390813

declared open · formalizederdos:774

True ↔ ∀ (A : Set ℕ), A.Infinite → A.IsProportionatelyDissociated → ∃ T, (∀ S ∈ T, S.IsDissociated) ∧ T.Finite ∧ A = ⋃₀ T

number theoryN/A2 sources

declared disproved (Lean) · formalizederdos:775

False ↔ ∃ C, ∃ᶠ (n : ℕ) in Filter.atTop, ∃ H, n - C ≤ H.cliqueSizes.ncard

graph theoryhypergraphspossible5 sources

declared openerdos:776

Erdős problem 776

combinatoricspossible2 sources

declared solvederdos:777

Erdős problem 777

graph theorycombinatoricsN/A

declared openerdos:778

Erdős problem 778

graph theoryN/A

declared falsifiable · formalizederdos:779

∀ n ≥ 1, have P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i; ∃ p, Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P

number theoryprimesA0052352 sources

declared provederdos:780

Erdős problem 780

combinatoricshypergraphschromatic numberN/A

declared disprovederdos:781

Erdős problem 781

additive combinatoricspossible

declared openerdos:782

Erdős problem 782

number theoryN/A

declared solvederdos:783

Erdős problem 783

number theoryN/A3 sources

declared solvederdos:784

Erdős problem 784

number theoryN/A

declared proved (Lean) · formalizederdos:785

True ↔ ∀ (A B : Set ℕ), A.Infinite → B.Infinite → Erdos785.IsExactAdditiveComplement A B → Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTop

additive combinatoricsN/A5 sources

declared open · formalizederdos:786

Erdos786.consecutivePrimesFrom 2 1 = {2, 3}

number theoryA143301 · possible2 sources

declared openerdos:787

Erdős problem 787

additive combinatoricspossible

declared openerdos:788

Erdős problem 788

additive combinatoricspossible3 sources

declared open · formalizederdos:789

(fun n => ↑(Erdos789.subsetSumThreshold n)) =Θ[Filter.atTop] sorry

additive combinatoricspossible2 sources

declared openerdos:790

Erdős problem 790

additive combinatoricspossible

declared openerdos:791

Erdős problem 791

additive combinatoricsA066063

declared openerdos:792

Erdős problem 792

additive combinatoricspossible2 sources

declared proved (Lean)erdos:793

Let

F(n)

be the largest

A\subseteq\{1,\dots,n\}

with

a\nmid bc

for distinct

a,b,c\in A

. Is

F(n)=\pi(n)+(C+o(1))\,n^{2/3}(\log n)^{-2}

for some constant

C

number theorypossible3 sources

declared disproved (Lean) · formalizederdos:794

False ↔ ∀ (n : ℕ) (H : Finset (Finset (Fin (3 * n)))), H.IsThreeUniform → n ^ 3 + 1 ≤ H.card → H.ContainsSubgraph 4 3 ∨ H.ContainsSubgraph 5 7

graph theoryhypergraphsturan numberN/A5 sources

declared provederdos:795

Erdős problem 795

number theorypossible

declared open · formalizederdos:796

g_3(n)

is the largest size of

A \subseteq [1,n]

with fewer than three representations of every product

a_1 a_2

, does its conjectured second-order normalized term converge? The candidate proof gives an explicit limit constant.

number theorypossible5 sources

declared provederdos:797

Erdős problem 797

graph theorychromatic numberpossible

declared proved (Lean) · formalizederdos:798

True ↔ (fun n => ↑(Erdos798.t n)) =o[Filter.atTop] fun n => ↑n

geometryA1164465 sources

declared provederdos:799

Erdős problem 799

graph theorychromatic numberN/A

declared provederdos:800

Erdős problem 800

graph theoryramsey theoryN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science