Vela Mathematics Program: problems

Narrowed tosource:gpt-erdos ×Clear all

Problem ledger

57 problems · 1/2Number SourcesGraph view

declared open · $100erdos:78

Erdős problem 78

graph theoryramsey theoryA0594422 sources

declared open · formalizederdos:91

(∀ᶠ (n : ℕ) in Filter.atTop, ¬Erdos91.UniqueMinimizer n) ↔ True

geometrydistancesA186704 · possible3 sources

declared open · formalized · $10000erdos:142

∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources

declared open · $500erdos:161

Erdős problem 161

combinatoricsramsey theorydiscrepancyN/A2 sources

declared open (Lean) · formalizederdos:180

For every finite family

\mathcal{F}

of graphs, is there a single

G \in \mathcal{F}

with

\mathrm{ex}(n;G) \ll_{\mathcal{F}} \mathrm{ex}(n;\mathcal{F})

? A counterexample refutes the Erdős-Simonovits compactness conjecture.

graph theoryturan numberN/A4 sources

declared open · formalizederdos:274

sorry ↔ ∀ (G : Type u_1) [inst : Group G], 1 < ENat.card G → ∀ (ι : Type u_2) [inst_1 : Fintype ι] (P : Erdos274.Group.ExactCovering G ι), 1 < Fintype.card ι → ∃ i j, i ≠ j ∧ Cardinal.mk ↥(P.parts i) = Cardinal.mk ↥(P.parts j)

group theorycovering systemsN/A3 sources

declared proved (Lean) · formalizederdos:281

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε

number theorycovering systemsN/A7 sources

declared open · formalizederdos:302

∀ (f : ℕ → ℕ), (∀ (N : ℕ), Erdos302.IsMaxNoTripleCard N (f N)) → Filter.Tendsto (fun N => ↑(f N) / ↑N) Filter.atTop (nhds sorry)

number theoryunit fractionsA3903953 sources

declared open · formalizederdos:332

∀ (A : Set ℕ), sorry A → Erdos332.HasBoundedGaps (Erdos332.D_A A)

number theoryN/A3 sources

declared openerdos:335

Erdős problem 335

number theoryadditive combinatoricsN/A2 sources

declared proved (Lean) · formalizederdos:369

True ↔ ∀ (ε : ℝ), 0 < ε → ∀ (k : ℕ), 2 ≤ k → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε

number theoryN/A7 sources

declared disproved (Lean) · formalizederdos:397

False ↔ {(M, N) | Disjoint M N ∧ ∏ i ∈ M, i.centralBinom = ∏ j ∈ N, j.centralBinom}.Finite

number theorybinomial coefficientsN/A7 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 open · formalizederdos:517

sorry ↔ ∀ {f : ℂ → ℂ} {n : ℕ → ℕ}, HasFabryGaps n → ∀ {a : ℕ → ℂ}, (∀ (k : ℕ), a k ≠ 0) → (∀ (z : ℂ), HasSum (fun k => a k * z ^ n k) (f z)) → ∀ (z : ℂ), {x | f x = z}.Infinite

analysisN/A3 sources

declared openerdos:524

Erdős problem 524

analysisprobabilitypolynomialsN/A3 sources

declared disproved · formalizederdos:533

False ↔ ∀ (δ : ℝ), 0 < δ → ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), G.CliqueFree 5 → δ * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ∃ S, c * ↑n ≤ ↑S.card ∧ G.CliqueFreeOn (↑S) 3

graph theoryN/A3 sources

declared open · formalizederdos:538

If each integer has at most

r

representations

m = pa

with

p

prime and

a \in A \subseteq [1, N]

, what is the best upper bound for

\sum_{a \in A} 1/a

? The candidate proof gives the matching order

\Theta_r(\log N / \log\log N)

number theoryN/A5 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 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 · formalized · $250erdos:591

True ↔ OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) 3

set theoryramsey theoryN/A3 sources

declared open · formalizederdos:602

¬Erdos602.disjoint_without_infinite_claim

combinatoricsset theoryN/A3 sources

declared verifiable · formalized · £25erdos:647

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

number theoryA062249 · A0872804 sources

declared provederdos:652

Erdős problem 652

geometrydistancesN/A2 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 openerdos:662

Among sufficiently large one-separated planar point sets, does the triangular lattice maximize the number of distances below each threshold? Explicit rational oblique lattices beat the triangular lattice under several closed- and strict-shell readings.

geometrydistancesN/A3 sources

declared openerdos:665

Erdős problem 665

combinatoricsN/A2 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 solvederdos:690

Erdős problem 690

number theorypossible4 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 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 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 openerdos:734

Erdős problem 734

combinatoricspossible2 sources

declared falsifiableerdos:743

Erdős problem 743

graph theoryN/A2 sources

declared solvederdos:783

Erdős problem 783

number theoryN/A3 sources

declared openerdos:788

Erdős problem 788

additive combinatoricspossible3 sources

declared openerdos:792

Erdős problem 792

additive combinatoricspossible2 sources

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 disproved · formalizederdos:847

False ↔ ∀ (A : Set ℕ), Infinite ↑A → Erdos847.HasFew3APs A → ∃ n S, (∀ (i : Fin n), ThreeAPFree (S i)) ∧ A = ⋃ i, S i

additive combinatoricsN/A3 sources

declared open · formalizederdos:850

True ↔ ∃ x y, x ≠ y ∧ x.primeFactors = y.primeFactors ∧ (x + 1).primeFactors = (y + 1).primeFactors ∧ (x + 2).primeFactors = (y + 2).primeFactors

number theoryprimesA3431013 sources

declared solvederdos:858

Erdős problem 858

number theoryprimitive setsN/A4 sources

declared openerdos:864

Erdős problem 864

number theorysidon setsadditive combinatoricsA3891822 sources

declared openerdos:866

Estimate the least excess

g_k(N)

forcing

k

integers whose pairwise sums all lie in a dense subset of

\{1, \dots, 2N\}

; in particular, determine the positive variant

h_4(n)

number theoryadditive combinatoricspossible5 sources

declared solved · formalizederdos:888

(fun n => ↑(Nat.findGreatest (Erdos888.p n) n)) =Θ[Filter.atTop] fun n => ↑n * Real.log (Real.log ↑n) / Real.log ↑n

number theorysquaresA3875845 sources

declared open · formalizederdos:893

True ↔ Filter.Tendsto (fun n => ↑(Erdos893.f (2 * n)) / ↑(Erdos893.f n)) Filter.atTop Filter.atTop

number theorydivisorsA046801 · possible3 sources

declared open · formalizederdos:906

Is there an entire non-zero function

f:\mathbb{C}\to \mathbb{C}

such that, for any infinite sequence

n_1<n_2<\cdots

, the set

\{ z: f^{(n_k)}(z)=0 \textrm{ for some }k\geq 1\}

is everywhere dense? The literal question is trivial for polynomials, so the claims address the transcendental entire case, in the affirmative.

analysisiterated functionsN/A5 sources

declared open · formalizederdos:943

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(AdditiveCombinatorics.sumRep Nat.Powerful n) ≤ ↑n ^ o n

number theorypossible4 sources

declared openerdos:954

Erdős problem 954

number theoryA3906422 sources

declared openerdos:969

Erdős problem 969

number theoryA0139282 sources

declared proved (Lean) · formalizederdos:1014

∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun l => ↑R(k, l + 1) / ↑R(k, l)) Filter.atTop (nhds 1)

graph theorypossible7 sources

declared provederdos:1021

Erdős problem 1021

graph theoryN/A2 sources

Problems · Vela Mathematics Program

Problem ledger