Vela Mathematics Program: problems

Narrowed toopen ×binomial coefficients ×Clear all

Problem ledger

14 problemsGraph view

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: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:396

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

number theorybinomial coefficientsA3750773 sources

declared open · formalizederdos:683

True ↔ ∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k < n → ↑(Erdos683.P n k) > min (↑n - ↑k + 1) (↑k ^ (1 + c))

number theoryprimesbinomial coefficientsA006530 · A074399 · A121359 · possible2 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 openerdos:685

Erdős problem 685

number theoryprimesbinomial coefficientsN/A

declared open · formalizederdos:700

∀ (n : ℕ), ¬Nat.Prime n → 1 < n → (Erdos700.f n = n / Erdos700.P n ↔ True)

number theorybinomial coefficientsA091963 · possible2 sources

declared open · formalizederdos:730

True ↔ Erdos730.S.Infinite

number theorybinomial coefficientsbase representationsA1295154 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 open · formalizederdos:849

True ↔ ∀ t ≥ 1, ∃ a, {n | ∃ k ≥ 1, 2 * k ≤ n ∧ n.choose k = a}.ncard = t

number theorybinomial coefficientsA003016 · A003015 · A059233 · A098565 · A090162 · A180058 · A1822372 sources

declared open · formalizederdos:1093

sorry ↔ {x | have k := x.1; have n := x.2; 2 * k ≤ n ∧ Erdos1093.deficiency n k = 1 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ n.choose k → k < p}.Infinite

number theorybinomial coefficientsN/A2 sources

declared open · formalizederdos:1094

{(n, k) | 0 < k ∧ 2 * k ≤ n ∧ (n.choose k).minFac > max (n / k) k}.Finite

number theorybinomial coefficientsN/A2 sources

declared open · formalizederdos:1095

Asymptotics.IsEquivalent Filter.atTop (fun k => Real.log ↑(Erdos1095.g k)) fun k => ↑k / Real.log ↑k

number theorybinomial coefficientsA0034584 sources

Problems · Vela Mathematics Program

Problem ledger