Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 5/12Number SourcesGraph view

declared provederdos:380

Erdős problem 380

number theoryA070003 · A388654 · A387054 · A3891003 sources

declared disprovederdos:381

Erdős problem 381

number theorydivisorsA002182

declared openerdos:382

Erdős problem 382

number theoryA388850

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 provederdos:384

Erdős problem 384

number theorybinomial coefficientsN/A

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 solved · formalizederdos:387

False ↔ ∃ c, 0 < c ∧ ∀ (n k : ℕ), 1 ≤ k → k < n → ∃ d, ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k

number theorybinomial coefficientsN/A2 sources

declared openerdos:388

Erdős problem 388

number theoryN/A2 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 provederdos:391

Erdős problem 391

number theoryfactorialsA034258 · A034259

declared proved (Lean) · formalizederdos:392

∀ (A : ℕ → ℕ), (∀ n > 0, IsLeast {x | ∃ t, ∃ (_ : ∃ a, n.factorial = ∏ i, a i ∧ Monotone a ∧ a (Fin.last t) ≤ n ^ 2), t + 1 = x} (A n)) → (fun n => ↑(A n) - ↑n / 2 + ↑n / (2 * Real.log ↑n)) =o[Filter.atTop] fun n => ↑n / Real.log ↑n

number theoryfactorialspossible5 sources

declared openerdos:393

Erdős problem 393

number theoryfactorialsA3883022 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 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 falsifiable · formalizederdos:398

sorry ↔ {n | ∃ m, n.factorial + 1 = m ^ 2} = {4, 5, 7}

number theoryfactorialsA146968 · A1413992 sources

declared disproved (Lean) · formalizederdos:399

False ↔ ¬∃ n x y k, 1 < x * y ∧ 2 < k ∧ (n.factorial = x ^ k + y ^ k ∨ n.factorial + y ^ k = x ^ k)

number theoryfactorialsN/A5 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 proved (Lean) · formalizederdos:401

True ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (r : ℕ), 1 ≤ r → {n | ∃ a₁ a₂, 0 < a₁ ∧ 0 < a₂ ∧ ↑a₁ + ↑a₂ > ↑n + f r * Real.log ↑n ∧ a₁.factorial * a₂.factorial ∣ n.factorial * (∏ i ∈ Finset.range r, Nat.nth Nat.Prime i) ^ n}.Infinite

number theoryfactorialsN/A6 sources

declared proved · formalizederdos:402

∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card

number theoryN/A2 sources

declared proved (Lean) · formalizederdos:403

True ↔ {p | (∀ a ∈ p.2, 0 < a) ∧ 2 ^ p.1 = ∑ a ∈ p.2, a.factorial}.Finite

number theoryfactorialsN/A4 sources

declared openerdos:404

Erdős problem 404

number theoryfactorialsN/A

declared provederdos:405

Erdős problem 405

number theoryfactorialsN/A

declared open · formalizederdos:406

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

number theorybase representationsN/A2 sources

declared provederdos:407

Erdős problem 407

number theorypossible · A387688

declared openerdos:408

Erdős problem 408

number theoryiterated functionsA049108

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

Erdős problem 411

number theoryiterated functionsA383044 · 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 openerdos:415

Erdős problem 415

number theorypossible2 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 proved (Lean) · formalizederdos:418

True ↔ {x | ∃ n, n - n.totient = x}ᶜ.Infinite

number theoryA005278 · A2639585 sources

declared solved (Lean) · formalizederdos:419

{x | MapClusterPt x Filter.atTop Erdos419.factorialDivisorRatio} = Erdos419.limitPointSet

number theoryfactorialsN/A5 sources

declared openerdos:420

Erdős problem 420

number theoryN/A

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

Erdős problem 423

number theoryA0052432 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 openerdos:425

Erdős problem 425

number theorysidon setspossible2 sources

declared proved (Lean) · formalizederdos:427

True ↔ Erdos427.erdos427

number theoryprimesN/A5 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 disproved (Lean) · formalizederdos:429

False ↔ ∃ f, Filter.Tendsto f Filter.atTop Filter.atTop ∧ ∀ (A : Set ℕ), A.Infinite → (∀ (N : ℕ), (A ∩ Set.Icc 1 N).ncard ≤ f N) → (∀ (p : ℕ), Nat.Prime p → ∃ b, ∀ a ∈ A, ↑a ≠ b) → ∃ n, ∀ a ∈ A, Nat.Prime (n + a)

number theoryN/A5 sources

declared openerdos:430

Erdős problem 430

number theorypossible

declared openerdos:431

Erdős problem 431

number theoryprimesN/A

Problems · Vela Mathematics Program

Problem ledger

Search problems.science