Vela Mathematics Program: problems

Narrowed toopen ×source:gpt-erdos ×Clear all

Problem ledger

35 problemsGraph 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 · 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 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 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 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 open · formalizederdos:602

¬Erdos602.disjoint_without_infinite_claim

combinatoricsset theoryN/A3 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 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 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 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 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 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 open · formalizederdos:1063

have upper_bound := sorry; (fun k => ↑(Erdos1063.n k)) =O[Filter.atTop] upper_bound ∧ upper_bound =o[Filter.atTop] fun k => ↑k * (Finset.Icc 1 (k - 1)).lcm fun n => ↑n

number theoryA3893603 sources

declared open · formalizederdos:1084

∀ {n : ℕ}, n ≠ 0 → Erdos1084.f 2 n < 3 * n

geometrydistancesA045945 · possible3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science