Vela Mathematics Program: problems

Narrowed toopen ×source:formal-conjectures ×Clear all

Problem ledger

319 problems · 3/7Number SourcesGraph view

declared open · formalizederdos:304

∀ {a b : ℕ}, 1 ∈ Erdos304.unitFractionExpressible a b → a ∣ b

number theoryunit fractionsA097847 · A0978492 sources

declared open · formalizederdos:306

a/b \in \mathbb{Q}_{>0}

and

b

is squarefree, can

a/b

always be written as a finite sum of reciprocals of distinct products of two distinct primes?

number theoryunit fractionsN/A4 sources

declared open · formalizederdos:312

True ↔ ∃ c, 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ N₀, ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K → ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:313

sorry ↔ Erdos313.erdos313Solutions.Infinite

number theoryunit fractionsA0543772 sources

declared open · formalizederdos:317

∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| ≥ 1 / ↑((Finset.Icc 1 n).lcm id)

number theoryunit fractionsN/A2 sources

declared open · formalizederdos:319

∀ (N : ℕ), IsGreatest {x | ∃ A, ∃ (_ : A ⊆ Finset.Icc 1 N) (_ : ∃ δ, ∑ n ∈ A, ↑↑(δ n) / ↑n = 0 ∧ ∀ A' ⊂ A, A'.Nonempty → ∑ n ∈ A', ↑↑(δ n) / ↑n ≠ 0), A.card = x} sorry

number theoryunit fractionspossible2 sources

declared open · formalizederdos:323

True ↔ ∀ k ≥ 1, ∀ ε > 0, (fun x => ↑x ^ (1 - ε)) =O[Filter.atTop] fun x => ↑(Erdos323.f k k x)

number theorypowersA004825 · A004831 · A004832 · A004833 · A004842 · A004843 · A004844 · A004845 · A004857 · A004869 · possible2 sources

declared open · formalizederdos:324

sorry ↔ ∃ f, Set.InjOn (fun x => match x with | (a, b) => Polynomial.eval (↑a) f + Polynomial.eval (↑b) f) {(a, b) | a < b}

number theorypowersN/A2 sources

declared open · formalizederdos:325

True ↔ ∀ (k : ℕ), 3 ≤ k → (fun x => ↑x ^ (3 / ↑k)) =O[Filter.atTop] fun x => ↑(Erdos325.cardIsSumThreePowerBelow k x)

number theorypowersA004825 · A004832 · A004843 · A004854 · A004865 · possible2 sources

declared open · formalizederdos:326

Does there exist

A=\{a_1<a_2<\cdots\}\subset \mathbb{N}

which is a minimal basis of order

2

(every large integer is the sum of

2

elements from

A

, and no proper subset of

A

has this property) such that

\lim_{k\to \infty}a_k/k^2=c

for some

c\neq 0

? A claimed construction gives a minimal basis with

A(x)=C\sqrt{x}+O(1)

, answering the question affirmatively; Erdős and Graham had conjectured a negative answer.

number theoryadditive basisN/A4 sources

declared open · formalizederdos:329

sSup {x | ∃ A, ∃ (_ : IsSidon A), Erdos329.sidonUpperDensity A = x} = sorry

number theorypossible2 sources

declared open · formalizederdos:332

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

number theoryN/A3 sources

declared open · formalizederdos:340

∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard

number theoryadditive combinatoricssidon setsA080200 · A0052822 sources

declared open · formalizederdos:341

True ↔ ∀ (a : ℕ → ℤ), (∀ᶠ (n : ℕ) in Filter.atTop, IsLeast {x | a n < x ∧ x ∉ {x | ∃ i ≤ n, ∃ j ≤ n, a i + a j = x}} (a (n + 1))) → have d := fun i => a (i + 1) - a i; ∃ p > 0, ∀ᶠ (m : ℕ) in Filter.atTop, d (m + p) = d m

number theoryN/A2 sources

declared open · formalizederdos:342

sorry ↔ ∀ (a : ℕ → ℕ), Erdos342.IsUlamSequence a → {n | ∃ m, a m = a n + 2}.Infinite

number theoryA0028583 sources

declared open · formalizederdos:346

Let

A=\{1\leq a_1< a_2<\cdots\}

be a set of integers such that

A\backslash B

is complete for any finite subset

B

and not complete for any infinite subset

B

. If

a_{n+1}/a_n \geq 1+\epsilon

for all

n

, must

\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2

? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

number theorycomplete sequencesN/A4 sources

declared open · formalizederdos:348

{x | ∃ m n, ∃ (_ : m < n), ∃ a, ∃ (_ : Monotone a) (_ : ∀ (s : Finset ℕ), s.card = m → IsAddComplete (Set.range (Function.updateFinset a s 0))) (_ : ∀ (t : Finset ℕ), t.card = n → ¬IsAddComplete (Set.range (Function.updateFinset a t 0))), (m, n) = x} = sorry

number theorycomplete sequencesN/A2 sources

declared open · formalizederdos:349

∀ (t α : ℝ), 0 < t → 2 < α → ¬Erdos349.IsGoodPair t α

number theorycomplete sequencesN/A3 sources

declared open · formalizederdos:352

True ↔ ∃ c > 0, ∀ (A : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet A → ↑(MeasureTheory.volume A) ≥ ↑c → ∃ t, (∀ (p : Fin 3), t.points p ∈ A) ∧ EuclideanGeometry.triangle_area (t.points 0) (t.points 1) (t.points 2) = 1

geometryN/A3 sources

declared open · formalizederdos:354

True ↔ ∀ α > 0, ∀ β > 0, Irrational (α / β) → IsAddCompleteNatSeq' (Erdos354.FloorMultiples.interleave α β 2)

number theoryN/A2 sources

declared open · formalizederdos:357

(fun n => ↑(Erdos357.f n)) =o[Filter.atTop] fun n => ↑n

number theoryA364132 · A364153 · possible2 sources

declared open · formalizederdos:359

∀ (A : ℕ → ℕ), Erdos359.IsGoodFor A 1 → Filter.Tendsto (fun k => ↑(A k) / ↑k) Filter.atTop Filter.atTop

number theoryA0020482 sources

declared open · formalizederdos:361

∀ (c : ℝ), 0 < c → Erdos361.subsetSumAvoidanceNumber c = sorry

number theorypossible2 sources

declared open · formalizederdos:371

{n | (n + 1).maxPrimeFac > n.maxPrimeFac}.HasDensity (1 / 2)

number theoryA0700892 sources

declared open · formalizederdos:373

Erdos373.S.Finite

number theoryfactorialsA0031352 sources

declared open · formalizederdos:376

True ↔ {n | n.centralBinom.Coprime 105}.Infinite

number theorybinomial coefficientsbase representationsA0309792 sources

declared open · formalizederdos:377

True ↔ ∃ C > 0, ∀ (n : ℕ), Erdos377.sumInvPrimesNotDvdCentralBinom n ≤ C

number theorybinomial coefficientsN/A2 sources

declared open · formalizederdos:383

True ↔ ∀ (k : ℕ), {p | Nat.Prime p ∧ (∏ i ∈ Finset.Icc 0 k, (p ^ 2 + i)).maxPrimeFac = p}.Infinite

number theoryN/A2 sources

declared open · formalizederdos:385

sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, n < Erdos385.F n

number theoryA3222922 sources

declared open · formalizederdos:386

True ↔ ∃ k ≥ 2, ∃ᶠ (n : ℕ) in Filter.atTop, k ≤ n - 2 ∧ ∃ p q, n.choose k = ∏ i ∈ Finset.Ico p q, Nat.nth Nat.Prime i

number theorybinomial coefficientsA2809922 sources

declared open · formalizederdos:389

True ↔ ∀ n ≥ 1, ∃ k ≥ 1, ∏ i ∈ Finset.range k, (n + i) ∣ ∏ i ∈ Finset.range k, (n + k + i)

number theoryA3750712 sources

declared open · formalizederdos:390

Let

f(n)

be the least

m

for which

n!

can be written as

a_1\cdots a_k

with

n < a_1 < \cdots < a_k = m

- the smallest possible largest factor in a factorization of

n!

into distinct integers all exceeding

n

. Erdős, Guy and Selfridge proved

f(n) - 2n \asymp n/\log n

. Erdős asked whether there is a constant

c

with

f(n) - 2n \sim c\,\frac{n}{\log n},

and what it is. This preprint answers yes and names the constant:

\lim_{n\to\infty}\frac{(f(n)-2n)\log n}{n} = \frac{4029639598}{25970038185} \approx 0.15516.

number theoryfactorialsA1934294 sources

declared open · formalizederdos:394

For the least

t_k(n)

with

n \mid t_k(n)(t_k(n)+1)\cdots(t_k(n)+k-1)

, do the conjectured logarithmic-saving and adjacent-length estimates hold on average? Both answered affirmatively, with

c = 1/2048

admissible in the

t_2

bound.

number theoryA3440054 sources

declared open · formalizederdos:396

True ↔ ∀ (k : ℕ), ∃ n, n.descFactorial (k + 1) ∣ n.centralBinom

number theorybinomial coefficientsA3750773 sources

declared open · formalizederdos:400

True ↔ ∀ k ≥ 2, ∃ c, Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.Icc 1 x, ↑(Erdos400.g k n)) fun x => c * ↑x * Real.log ↑x

number theoryfactorialspossible3 sources

declared open · formalizederdos:406

True ↔ {n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1]}.Finite

number theorybase representationsN/A2 sources

declared open · formalizederdos:409

∀ (n : ℕ), 0 < n → IsLeast {i | Nat.Prime ((fun x => x.totient + 1)^[i] n)} sorry

number theoryiterated functionsA039651 · A2294872 sources

declared open · formalizederdos:410

True ↔ ∀ n > 1, Filter.Tendsto (fun k => ↑((⇑(ArithmeticFunction.sigma 1))^[k] n) ^ (1 / ↑k)) Filter.atTop Filter.atTop

number theoryiterated functionsA007497 · possible2 sources

declared open · formalizederdos:412

True ↔ ∀ m ≥ 2, ∀ n ≥ 2, ∃ i j, (⇑(ArithmeticFunction.sigma 1))^[i] m = (⇑(ArithmeticFunction.sigma 1))^[j] n

number theoryiterated functionsA007497 · A0515722 sources

declared open · formalizederdos:413

True ↔ {n | Erdos413.IsBarrier (fun m => ↑(ArithmeticFunction.cardDistinctFactors m)) n}.Infinite

number theoryiterated functionsA0052362 sources

declared open · formalizederdos:414

True ↔ ∀ m > 0, ∀ n > 0, ∃ i j, Erdos414.h^[i] m = Erdos414.h^[j] n

number theoryiterated functionsA064491 · possible2 sources

declared open · formalizederdos:416

Filter.Tendsto (fun x => Erdos416.V (2 * x) / Erdos416.V x) Filter.atTop (nhds 2)

number theoryA2648102 sources

declared open · formalizederdos:417

True ↔ ∃ L, Filter.Tendsto (fun x => ↑{k | k ∈ Set.range Nat.totient ∧ ↑k ≤ x}.ncard / ↑(Nat.totient '' {m | 1 ≤ m ∧ ↑m ≤ x}).ncard) Filter.atTop (nhds L)

number theoryA264810 · A0610702 sources

declared open · formalizederdos:421

True ↔ ∃ d, StrictMono d ∧ 1 ≤ d 0 ∧ (Set.range d).HasDensity 1 ∧ Set.InjOn (fun x => match x with | (u, v) => ∏ i ∈ Finset.Icc u v, d i) {(u, v) | u ≤ v}

number theoryA389544 · A3908482 sources

declared open · formalizederdos:422

True ↔ {n | ∀ (x : ℕ+), Erdos422.f x ≠ n}.Infinite

number theoryA0051852 sources

declared open · formalizederdos:424

Let

a_1 = 2

and

a_2 = 3

and continue the sequence by appending to

a_1, \dots, a_n

all possible values of

a_ia_j - 1

with

i \ne j

. Is it true that the set of integers which eventually appear has positive density?

number theoryA0052444 sources

declared open · formalizederdos:428

True ↔ ∃ A, (∃ᶠ (n : ℕ) in Filter.atTop, ∀ a ∈ A, 0 < a → a < n → Nat.Prime (n - a)) ∧ Filter.liminf (fun n => Erdos428.primeDensityRatio A n) Filter.atTop > 0

number theoryprimesN/A2 sources

declared open · formalizederdos:445

True ↔ ∀ c > 1 / 2, ∀ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p → ∀ (n : ℕ), Erdos445.Erdos445Prop c p n

number theoryN/A2 sources

declared open · formalizederdos:450

How large must

y(\varepsilon, n)

be so that every interval

(x, x+y)

contains at most

\varepsilon y

integers having a divisor in

(n, 2n)

? The candidate proof gives the sharp fixed-

\varepsilon

order

y = \Theta_\varepsilon(n)

, uniformly in the translate.

number theorydivisorsN/A4 sources

declared open · formalizederdos:454

True ↔ Filter.limsup (fun n => ↑(Erdos454.f n) - 2 * ↑(Nat.nth Prime n)) Filter.atTop = ⊤

number theoryprimesA389676 · A3896772 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science