Vela Mathematics Program: problems

Narrowed tosource:erdos-ai-contributions-wiki ×Clear all

Problem ledger

353 problems · 4/8Number SourcesGraph view

declared disproved (Lean) · formalizederdos:505

∃ n S, Bornology.IsBounded S ∧ 0 < Metric.diam S ∧ ∀ (F : Fin (n + 1) → Set (EuclideanSpace ℝ (Fin n))), S ⊆ ⋃ i, F i → ∃ i, Metric.diam S ≤ Metric.diam (F i)

geometrypossible5 sources

declared open · formalizederdos:507

Asymptotics.IsEquivalent Filter.atTop Erdos507.α sorry

geometryN/A3 sources

declared proved (Lean) · formalizederdos:512

True ↔ ∃ c > 0, ∀ (N : ℕ) (A : Finset ℤ), A.card = N → c * Real.log ↑N ≤ ∫ (θ : ℝ) in 0..1, ‖∑ n ∈ A, additiveChar (↑n * θ)‖

analysisN/A4 sources

declared open · formalizederdos:513

sorry = ⨆ f, Filter.liminf (fun r => Erdos513.ratio r ↑f) Filter.atTop

analysisN/A3 sources

declared openerdos:514

For a transcendental entire function, how fast can

|f(z)|

be forced to grow along a path to infinity, and how short can such a path be in terms of the maximum modulus

M(r, f)

analysisN/A4 sources

declared proved (Lean) · formalizederdos:519

True ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ k, c < ‖Erdos519.powerSum z (↑k + 1)‖

analysisN/A5 sources

declared open · formalizederdos:521

False ↔ Erdos521.Claim

analysispolynomialsprobabilityN/A4 sources

declared openerdos:524

Erdős problem 524

analysisprobabilitypolynomialsN/A3 sources

declared open · formalizederdos:535

∀ r ≥ 3, ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos535.f r N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))

number theorypossible3 sources

declared open · formalizederdos:536

True ↔ ∀ ε > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ε * ↑N ≤ ↑A.card → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, {a, b, c}.card = 3 ∧ a.lcm b = b.lcm c ∧ b.lcm c = a.lcm c

number theorypossible3 sources

declared disproved (Lean) · formalizederdos:537

False ↔ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ ε * ↑N → ∃ a₁ ∈ A, ∃ a₂ ∈ A, ∃ a₃ ∈ A, ∃ p₁ p₂ p₃, Nat.Prime p₁ ∧ Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ p₁ ≠ p₂ ∧ p₁ ≠ p₃ ∧ p₂ ≠ p₃ ∧ a₁ * p₁ = a₂ * p₂ ∧ a₂ * p₂ = a₃ * p₃

number theorypossible5 sources

declared open · formalizederdos:539

For

|A| = n

, how small can the cofactor set

Q(A) = \{a / \gcd(a,b) : a, b \in A\}

be? The answer is

h(n) = n^{1/2 + o(1)}

: a new upper bound

h(n) \le n^{1/2} \exp(O(\sqrt{\log n}))

matches the classical lower bound.

number theorypossible5 sources

declared proved (Lean) · formalizederdos:540

True ↔ ∃ C, 0 < C ∧ ∀ (N : ℕ), 0 < N → ∀ (A : Finset (ZMod N)), C * √↑N ≤ ↑A.card → Erdos540.HasZeroSubsetSum A

number theoryA0344635 sources

declared proved (Lean) · formalizederdos:541

True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (a : Fin p → ZMod p), (∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2

number theoryN/A5 sources

declared disprovederdos:543

Erdős problem 543

number theorygroup theorypossible3 sources

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 proved (Lean) · formalized · $100erdos:582

True ↔ ∃ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G

graph theoryramsey theoryN/A5 sources

declared open · formalized · $500erdos:593

Erdos Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. The answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Problem #1177 on exact spectra is settled alongside it.

set theorygraph theoryhypergraphsN/A4 sources

declared open · formalizederdos:598

∀ (m : Type u_1) [Infinite m], True ↔ ∃ c, ∀ (X : Set m), Cardinal.mk ↑X = Erdos598.κ → c '' {s | ↑s ⊆ X} = Set.univ

set theoryramsey theoryN/A3 sources

declared solvederdos:603

Erdős problem 603

combinatoricsset theoryN/A3 sources

declared proved (Lean)erdos:610

Erdős problem 610

graph theorypossible4 sources

declared disproved (Lean) · formalizederdos:613

False ↔ ∀ n ≥ 3, ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], G.edgeFinset.card = (2 * n + 1).choose 2 - n.choose 2 - 1 → ∃ B D, ∀ [DecidableRel B.Adj] [inst_3 : DecidableRel D.Adj], G = B ⊔ D ∧ B.IsBipartite ∧ ∀ (v : V), D.degree v < n

graph theoryN/A5 sources

declared openerdos:616

Erdős problem 616

graph theoryN/A2 sources

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 openerdos:629

Erdős problem 629

graph theorychromatic numberpossible2 sources

declared openerdos:635

Erdős problem 635

number theoryN/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 openerdos:654

n

planar points have no four concyclic, must some point determine

(1 - o(1))n

distinct distances? Failing that, can one always force more than

(1/3 + c)n

geometrydistancespossible3 sources

declared proved (Lean)erdos:658

Erdős problem 658

additive combinatoricspossible4 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 open · $250erdos:671

For triangular arrays of nodes

a_i^n\in[-1,1]

let

\mathcal{L}^nf

be the Lagrange interpolation polynomials of a continuous

f

, with fundamental polynomials

p_i^n

. Is there a choice of nodes such that for every continuous

f

there is some

x

where

\limsup_n \sum_i\lvert p_{i}^n(x)\rvert=\infty

and yet

\mathcal{L}^nf(x) \to f(x)

? Is there a choice with

\limsup_n \sum_i\lvert p_{i}^n(x)\rvert=\infty

for every

x

, yet for every continuous

f

some

x

has

\mathcal{L}^nf(x)\to f(x)

? Both questions are claimed resolved in the affirmative.

analysisN/A3 sources

declared openerdos:675

Erdős problem 675

number theoryN/A2 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 openerdos:679

Erdős problem 679

number theoryN/A2 sources

declared openerdos:684

For the least

k

at which the small-prime part of

\binom{n}{k}

exceeds

n^2

, how large can

f(n)

be?

number theoryprimesbinomial coefficientsA392019 · possible3 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: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 solvederdos:690

Erdős problem 690

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

Problems · Vela Mathematics Program

Problem ledger

Search problems.science