Vela Mathematics Program: problems

Problem ledger

1,217 problems · 15/25Number SourcesGraph view

declared open · formalizederdos:701

True ↔ ∀ {X : Type} [Nonempty X] [Fintype X] (F : Set (Set X)), IsLowerSet F → ∃ x, ∀ F' ⊆ F, F'.Intersecting → Cardinal.mk ↑F' ≤ Cardinal.mk ↑{A | A ∈ F ∧ x ∈ A}

combinatoricsintersecting familyN/A2 sources

declared provederdos:702

Erdős problem 702

combinatoricsN/A

declared proved · $250erdos:703

Erdős problem 703

combinatoricsA390645

declared openerdos:704

Erdős problem 704

graph theorygeometrychromatic numberN/A

declared disproved · formalizederdos:705

False ↔ ∃ k, ∀ (V : Set (EuclideanSpace ℝ (Fin 2))), V.Finite → (SimpleGraph.UnitDistancePlaneGraph V).girth ≥ k → (SimpleGraph.UnitDistancePlaneGraph V).chromaticNumber ≤ 3

graph theorychromatic numberN/A3 sources

declared openerdos:706

Erdős problem 706

graph theorychromatic numberpossible

declared disproved (Lean) · formalized · $1000erdos:707

Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a 1000 dollars prize attached, that every finite Sidon set extends to a perfect difference set modulo

p^2+p+1

for some prime

p

. Alexeev and Mixon establish that

\{1,2,4,8\}

is a counterexample - and discovered along the way that Marshall Hall, Jr. had published a different counterexample three decades before Erdős first posed the problem, unnoticed by the community for half a century.

additive combinatoricssidon setsN/A6 sources

declared open · $100erdos:708

Erdős problem 708

number theorypossible

declared openerdos:709

How long must an interval be to contain distinct representatives

x_i

, with

a_i \mid x_i

, for every

n

-element set of moduli

A = \{a_1, \dots, a_n\}

number theorypossible2 sources

declared open · ₹2000erdos:710

Erdős problem 710

number theoryA390246

declared open · ₹1000erdos:711

Erdős problem 711

number theorypossible

declared open · $500erdos:712

Erdős problem 712

graph theoryturan numberhypergraphspossible

declared open · $500erdos:713

Erdős problem 713

graph theoryturan numberN/A

declared openerdos:714

Erdős problem 714

graph theoryturan numberpossible

declared provederdos:715

Erdős problem 715

graph theoryN/A

declared proved (Lean)erdos:716

Erdős problem 716

graph theoryhypergraphspossible3 sources

declared provederdos:717

Erdős problem 717

graph theoryN/A

declared provederdos:718

Erdős problem 718

graph theoryN/A

declared openerdos:719

Erdős problem 719

graph theoryhypergraphspossible

declared proved · $100erdos:720

Erdős problem 720

graph theoryramsey theorypossible

declared solvederdos:721

Erdős problem 721

number theoryadditive combinatoricsramsey theoryA171081

declared provederdos:722

Erdős problem 722

combinatoricsN/A

declared falsifiable · formalizederdos:723

True ↔ ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L) (pp : Configuration.ProjectivePlane P L), IsPrimePow (Configuration.ProjectivePlane.order P L)

combinatoricsN/A2 sources

declared openerdos:724

Erdős problem 724

combinatoricsA001438

declared openerdos:725

Erdős problem 725

combinatoricsA001009

declared open · formalizederdos:726

True ↔ Asymptotics.IsEquivalent Filter.atTop (fun n => ∑ p ∈ Finset.range (n + 1) with Nat.Prime p ∧ ↑p / 2 < ↑n % ↑p, 1 / ↑p) fun n => Real.log (Real.log ↑n) / 2

number theoryN/A3 sources

declared open · formalizederdos:727

True ↔ ∀ k ≥ 2, {n | (n + k).factorial ^ 2 ∣ (2 * n).factorial}.Infinite

number theoryfactorialsA002503 · A343507 · A3893962 sources

declared proved (Lean) · formalizederdos:728

Whether there are infinitely many integers

a, b, n

with

a, b \ge \varepsilon n

such that

a!\cdot b!

divides

n!\cdot(a+b-n)!

while

a+b

exceeds

n

by more than

C\cdot\log n

number theoryfactorialsN/A6 sources

declared proved (Lean) · formalizederdos:729

True ↔ ∀ C > 0, ∃ K ≥ 3, {(a, b, n) | a > 0 ∧ b > 0 ∧ n > 0 ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ∀ (p : ℕ), Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite

number theoryfactorialsN/A6 sources

declared open · formalizederdos:730

True ↔ Erdos730.S.Infinite

number theorybinomial coefficientsbase representationsA1295154 sources

declared openerdos:731

Let

A(n)

be the least positive integer not dividing

\binom{2n}{n}

. Erdos asked for the behaviour of

A(n)

for reasonable

n

. Under an explicit dyadic-regularity formalization of reasonable, the distribution is determined on dyadic intervals against the scale

F_X = \sqrt{2}(\log 2)^{1/4} L^{1/4} \exp\sqrt{(\log 2)L}

with

L = \log(2X)

number theorybinomial coefficientsA0061974 sources

declared provederdos:732

Erdős problem 732

combinatoricsN/A

declared provederdos:733

Erdős problem 733

combinatoricsgeometrypossible

declared openerdos:734

Erdős problem 734

combinatoricspossible2 sources

declared solvederdos:735

Erdős problem 735

geometryN/A

declared not provableerdos:736

Erdős problem 736

graph theorychromatic numberN/A

declared provederdos:737

Erdős problem 737

graph theorychromatic numberN/A

declared openerdos:738

Erdős problem 738

graph theorychromatic numberN/A

declared not provableerdos:739

Erdős problem 739

graph theorychromatic numberN/A

declared open · formalizederdos:740

True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 ≤ G.chromaticCardinal → ∀ (r : ℕ), ∃ H, H.coe.chromaticCardinal = G.chromaticCardinal ∧ Erdos740.NoShortOddCycle H.coe r

graph theorychromatic numberN/A2 sources

declared solved (Lean) · formalizederdos:741

True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

additive combinatoricsN/A6 sources

declared decidable · formalizederdos:742

∀ (a b : ℕ), (completeBipartiteGraph (Fin a) (Fin b)).edgeSet.ncard = a * b

graph theoryN/A2 sources

declared falsifiableerdos:743

Erdős problem 743

graph theoryN/A2 sources

declared disprovederdos:744

Erdős problem 744

graph theorychromatic numberpossible

declared provederdos:745

Erdős problem 745

graph theoryN/A

declared provederdos:746

Erdős problem 746

graph theoryN/A

declared solvederdos:747

Erdős problem 747

combinatoricshypergraphsN/A

declared provederdos:748

Erdős problem 748

number theoryA007865

declared open · formalizederdos:749

True ↔ ∀ ε > 0, ∃ A, 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun n => 1

additive combinatoricsN/A3 sources

declared proved (Lean) · formalizederdos:750

True ↔ ∀ (f : ℕ → NNReal), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ V G, G.chromaticNumber = ⊤ ∧ ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m → ∃ I ⊆ S, G.IsIndepSet I ∧ ↑m / 2 - f m ≤ ↑I.ncard

graph theorychromatic numberN/A5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science