Vela Mathematics Program: problems

Narrowed toformalized ×source:formal-conjectures ×Clear all

Problem ledger

604 problems · 8/13Number SourcesGraph view

declared proved (Lean) · formalizederdos:618

True ↔ ∀ (G : (n : ℕ) → SimpleGraph (Fin n)), (∀ (n : ℕ), (G n).CliqueFree 3) → ((fun n => ↑(G n).maxDegree) =o[Filter.atTop] fun n => ↑n ^ (1 / 2)) → (fun n => ↑(Erdos618.h2 (G n))) =o[Filter.atTop] fun n => ↑n ^ 2

graph theoryN/A5 sources

declared solved (Lean) · formalizederdos:619

False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] (G : SimpleGraph V), G.Connected → G.CliqueFree 3 → ↑(Erdos619.minNewEdges 4 G) < (1 - c) * ↑(Fintype.card V)

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:621

True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ), IsGreatest {k | ∃ A ⊆ G.edgeFinset, A.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → ({s(x, y), s(y, z), s(x, z)} ∩ A).card ≤ 1} a → IsLeast {k | ∃ T ⊆ G.edgeFinset, T.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → (T ∩ {s(x, y), s(y, z), s(x, z)}).Nonempty} t → 4 * (a + t) ≤ n ^ 2

graph theoryN/A5 sources

declared open · formalizederdos:623

Let

X

be a set of cardinality

\aleph_\omega

and

f

a function from the finite subsets of

X

X

such that

f(A)\not\in A

for all

A

. Must there exist an infinite independent

Y\subseteq X

, i.e. with

f(B)\not\in Y

for all finite

B\subset Y

? Claimed resolution: the positive assertion is equivalent to Koepke's free-subset property, hence independent of ZFC, with consistency strength exactly a measurable cardinal.

set theoryN/A4 sources

declared open · formalizederdos:624

Filter.Tendsto (fun n => ↑(Erdos624.H n) - Real.logb 2 ↑n) Filter.atTop Filter.atTop

combinatoricspossible2 sources

declared falsifiable · formalizederdos:628

∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V) (k : ℕ), G.chromaticNumber = ↑k → G.CliqueFree k → ∀ (a b : ℕ), a ≥ 2 → b ≥ 2 → a + b = k + 1 → ∃ s, (SimpleGraph.induce s G).chromaticNumber ≥ ↑a ∧ (SimpleGraph.induce sᶜ G).chromaticNumber ≥ ↑b

graph theorychromatic numberN/A2 sources

declared solved · formalized · $25erdos:633

∀ {n : ℕ} {T : Affine.Triangle ℝ (EuclideanSpace ℝ (Fin 2))}, Erdos633.IsCuttable n T → n ≠ 0

geometryN/A2 sources

declared proved (Lean) · formalizederdos:639

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Sym2 (Fin n) → Fin 2), {e | ¬e.IsDiag ∧ ∀ (x y : Fin n), e = s(x, y) → ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4

graph theoryramsey theoryN/A5 sources

declared proved (Lean) · formalizederdos:645

∀ (c : ℕ → Bool), ∃ x d, 0 < x ∧ x < d ∧ ∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared proved (Lean) · formalizederdos:646

True ↔ ∀ (S : Finset ℕ), (∀ p ∈ S, Nat.Prime p) → {n | ∀ p ∈ S, Even (padicValNat p n.factorial)}.Infinite

number theoryfactorialsN/A5 sources

declared verifiable · formalized · £25erdos:647

sorry ↔ ∃ n > 24, ⨆ m, ↑m + (ArithmeticFunction.sigma 0) ↑m ≤ n + 2

number theoryA062249 · A0872804 sources

declared solved (Lean) · formalizederdos:648

(fun n => ↑(Erdos648.g n)) =Θ[Filter.atTop] fun n => √(↑n / Real.log ↑n)

number theoryA3917505 sources

declared disproved (Lean) · formalizederdos:649

False ↔ ∀ (p q : ℕ), Nat.Prime p → Nat.Prime q → ∃ n, n.maxPrimeFac = p ∧ (n + 1).maxPrimeFac = q

number theorypossible5 sources

declared solved (Lean) · formalizederdos:650

∀ (m : ℕ), Erdos650.f m = min m ⌈2 * √↑m⌉₊

number theoryA0274346 sources

declared open · formalizederdos:653

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (1 - o n) * ↑n ≤ ↑(EuclideanGeometry.maximalDistinctDistancesFrom n)

geometrydistancespossible2 sources

declared open · formalizederdos:655

False ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))), X.card = n → Erdos655.IsValid X → (1 + c) * ↑n / 2 ≤ ↑(EuclideanGeometry.distinctDistances X)

geometrydistancespossible3 sources

declared proved (Lean) · formalizederdos:659

True ↔ ∃ A, (∀ (n : ℕ), (A n).card = n ∧ ∀ S ⊆ A n, S.card = 4 → 3 ≤ EuclideanGeometry.distinctDistances S) ∧ (fun n => ↑(EuclideanGeometry.distinctDistances (A n))) =O[Filter.atTop] fun n => ↑n / √(Real.log ↑n)

geometrydistancespossible6 sources

declared disproved (Lean) · formalizederdos:666

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ H ≤ SimpleGraph.hypercube n, ε * ↑n * 2 ^ (n - 1) ≤ ↑H.edgeSet.ncard → (SimpleGraph.cycleGraph 6).IsContained H

graph theorypossible5 sources

declared verifiable · formalizederdos:672

True ↔ ∀ (k l : ℕ), l > 1 → k ≥ 4 → Erdos672.Erdos672With k l

number theoryN/A2 sources

declared proved (Lean) · formalizederdos:674

True ↔ Erdos674.solutionSet.Nonempty

number theoryN/A4 sources

declared open · formalizederdos:677

∀ (m n k : ℕ), k > 0 → m ≥ n + k → Finset.lcmInterval m k ≠ Finset.lcmInterval n k

number theorypossible2 sources

declared proved (Lean) · formalizederdos:678

True ↔ ∀ᶠ (k : ℕ) in Filter.atTop, {(m, n) | n + k ≤ m ∧ Finset.lcmInterval m (k + 1) < Finset.lcmInterval n k}.Nonempty

number theorypossible5 sources

declared open · formalizederdos:680

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k, k ≠ 0 ∧ (n + k).minFac > k ^ 2 + 1

number theoryprimesN/A2 sources

declared open · formalizederdos:681

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ k > 0, (n + k).Composite ∧ ∀ (p : ℕ), Erdos681.IsLPF p (n + k) → p > k ^ 2

number theoryprimesA3896802 sources

declared open · formalizederdos:683

True ↔ ∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k < n → ↑(Erdos683.P n k) > min (↑n - ↑k + 1) (↑k ^ (1 + c))

number theoryprimesbinomial coefficientsA006530 · A074399 · A121359 · possible2 sources

declared open · formalizederdos:686

sorry ↔ ∀ N ≥ 2, ∃ k ≥ 2, ∃ n, ∃ m ≥ n + k, ↑N = ↑(∏ i ∈ Finset.Icc 1 k, (m + i)) / ↑(∏ i ∈ Finset.Icc 1 k, (n + i))

number theoryN/A4 sources

declared open · formalizederdos:688

sorry =O[Filter.atTop] Erdos688.epsilonFunction

number theoryN/A2 sources

declared open · formalizederdos:689

sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, ∀ m ∈ Finset.Icc 1 n, 2 ≤ {p ∈ Finset.Icc 1 n | Nat.Prime p ∧ a p ≡ m [MOD p]}.card

number theoryN/A3 sources

declared disproved (Lean) · formalizederdos:692

False ↔ ∀ (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → ∀ (n : ℕ), UnimodularOn (δ n) (n + 1)

number theorydivisorsN/A5 sources

declared solved (Lean) · formalizederdos:694

∀ (fmax fmin : ℕ → ℕ), (∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) → (∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) → ∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ ∀ (x : ℕ), sSup {x_1 | ∃ n, ∃ (_ : n ≤ x) (_ : ∃ m, m.totient = n), ↑(fmax n) / ↑(fmin n) = x_1} = (Real.exp Real.eulerMascheroniConstant + o x) * Real.log (Real.log ↑x)

number theorypossible6 sources

declared open · formalizederdos:695

sorry ↔ ∀ {q : ℕ → ℕ}, StrictMono q → (∀ (i : ℕ), Nat.Prime (q i)) → (∀ (i : ℕ), q (i + 1) % q i = 1) → Filter.Tendsto (fun k => ↑(q k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

number theoryA0610922 sources

declared proved · formalizederdos:697

∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

number theorydivisorsN/A2 sources

declared proved (Lean) · formalizederdos:698

True ↔ ∃ h, Filter.Tendsto h Filter.atTop Filter.atTop ∧ ∀ (n i j : ℕ), 2 ≤ i → i < j → j ≤ n / 2 → h n ≤ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientspossible5 sources

declared falsifiable · formalizederdos:699

True ↔ ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → ∃ p, Nat.Prime p ∧ i ≤ p ∧ p ∣ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientsN/A2 sources

declared open · formalizederdos:700

∀ (n : ℕ), ¬Nat.Prime n → 1 < n → (Erdos700.f n = n / Erdos700.P n ↔ True)

number theorybinomial coefficientsA091963 · possible2 sources

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

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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science