Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 8/12Number SourcesGraph view

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 · $1000erdos:687

Erdős problem 687

number theoryA048670 · A058989

declared open · formalizederdos:688

sorry =O[Filter.atTop] Erdos688.epsilonFunction

number theoryN/A2 sources

declared open · formalizederdos:689

sorry ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, ∀ m ∈ Finset.Icc 1 n, 2 ≤ {p ∈ Finset.Icc 1 n | Nat.Prime p ∧ a p ≡ m [MOD p]}.card

number theoryN/A3 sources

declared solvederdos:690

Erdős problem 690

number theorypossible4 sources

declared openerdos:691

Erdős problem 691

number theoryN/A

declared disproved (Lean) · formalizederdos:692

False ↔ ∀ (δ : ℕ → ℕ → ℝ), (∀ (a b : ℕ), Erdos692.IsDelta₁ a b (δ a b)) → ∀ (n : ℕ), UnimodularOn (δ n) (n + 1)

number theorydivisorsN/A5 sources

declared openerdos:693

Erdős problem 693

number theorydivisorsA391118 · possible

declared solved (Lean) · formalizederdos:694

∀ (fmax fmin : ℕ → ℕ), (∀ (n : ℕ), IsGreatest (Nat.totient ⁻¹' {n}) (fmax n)) → (∀ (n : ℕ), IsLeast (Nat.totient ⁻¹' {n}) (fmin n)) → ∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ ∀ (x : ℕ), sSup {x_1 | ∃ n, ∃ (_ : n ≤ x) (_ : ∃ m, m.totient = n), ↑(fmax n) / ↑(fmin n) = x_1} = (Real.exp Real.eulerMascheroniConstant + o x) * Real.log (Real.log ↑x)

number theorypossible6 sources

declared open · formalizederdos:695

sorry ↔ ∀ {q : ℕ → ℕ}, StrictMono q → (∀ (i : ℕ), Nat.Prime (q i)) → (∀ (i : ℕ), q (i + 1) % q i = 1) → Filter.Tendsto (fun k => ↑(q k) ^ (1 / ↑k)) Filter.atTop Filter.atTop

number theoryA0610922 sources

declared solved (Lean)erdos:696

Erdős problem 696

number theorydivisorspossible4 sources

declared proved · formalizederdos:697

∀ (m : ℕ) (α : ℝ), ∃ δ, {n | ∃ d, d ≡ 1 [MOD m] ∧ ↑d ∈ Set.Ioo 1 (Real.exp (↑m ^ α)) ∧ d ∣ n}.HasDensity δ

number theorydivisorsN/A2 sources

declared proved (Lean) · formalizederdos:698

True ↔ ∃ h, Filter.Tendsto h Filter.atTop Filter.atTop ∧ ∀ (n i j : ℕ), 2 ≤ i → i < j → j ≤ n / 2 → h n ≤ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientspossible5 sources

declared falsifiable · formalizederdos:699

True ↔ ∀ (n i j : ℕ), 1 ≤ i → i < j → j ≤ n / 2 → ∃ p, Nat.Prime p ∧ i ≤ p ∧ p ∣ (n.choose i).gcd (n.choose j)

number theorybinomial coefficientsN/A2 sources

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 · $100erdos:708

Erdős problem 708

number theorypossible

declared openerdos:709

How long must an interval be to contain distinct representatives

x_i

, with

a_i \mid x_i

, for every

n

-element set of moduli

A = \{a_1, \dots, a_n\}

number theorypossible2 sources

declared open · ₹2000erdos:710

Erdős problem 710

number theoryA390246

declared open · ₹1000erdos:711

Erdős problem 711

number theorypossible

declared solvederdos:721

Erdős problem 721

number theoryadditive combinatoricsramsey theoryA171081

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 open · formalizederdos:727

True ↔ ∀ k ≥ 2, {n | (n + k).factorial ^ 2 ∣ (2 * n).factorial}.Infinite

number theoryfactorialsA002503 · A343507 · A3893962 sources

declared proved (Lean) · formalizederdos:728

Whether there are infinitely many integers

a, b, n

with

a, b \ge \varepsilon n

such that

a!\cdot b!

divides

n!\cdot(a+b-n)!

while

a+b

exceeds

n

by more than

C\cdot\log n

number theoryfactorialsN/A6 sources

declared proved (Lean) · formalizederdos:729

True ↔ ∀ C > 0, ∃ K ≥ 3, {(a, b, n) | a > 0 ∧ b > 0 ∧ n > 0 ∧ ↑a + ↑b > ↑n + C * Real.log ↑n ∧ ∀ (p : ℕ), Nat.Prime p → p > K → padicValNat p (↑n.factorial / (↑a.factorial * ↑b.factorial)).den = 0}.Infinite

number theoryfactorialsN/A6 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 provederdos:748

Erdős problem 748

number theoryA007865

declared disprovederdos:763

Erdős problem 763

number theoryadditive combinatoricsN/A

declared disprovederdos:764

Erdős problem 764

number theoryadditive combinatoricsN/A

declared openerdos:768

Let

A(x)

count

n \le x

such that every prime

p \mid n

has a divisor

d > 1

n

with

d \equiv 1 \pmod p

. Erdos asked whether

A(x)/x = \exp(-(c+o(1))\sqrt{\log x}\log\log x)

. It does, with

c = 1/(2\sqrt{\log 2})

number theoryA001034 · A3522873 sources

declared open · formalizederdos:769

For the least cutoff

c(n)

after which every

k

occurs as the number of homothetic cubes in a decomposition of the unit

n

-cube, is

c(n) \gg n^n

? The Lean proof shows

c(n) = o(n^n)

along odd dimensions.

number theorygeometryA014544 · possible4 sources

declared open · formalizederdos:770

∀ {n : ℕ}, 2 < n → (Erdos770.h n = ↑n + 1 ↔ Nat.Prime (n + 1))

number theoryA263647 · possible2 sources

declared provederdos:771

Erdős problem 771

number theorypossible

declared provederdos:772

Erdős problem 772

number theorysidon setsadditive combinatoricspossible

declared openerdos:773

Erdős problem 773

number theorysidon setssquaresA390813

declared open · formalizederdos:774

True ↔ ∀ (A : Set ℕ), A.Infinite → A.IsProportionatelyDissociated → ∃ T, (∀ S ∈ T, S.IsDissociated) ∧ T.Finite ∧ A = ⋃₀ T

number theoryN/A2 sources

declared falsifiable · formalizederdos:779

∀ n ≥ 1, have P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i; ∃ p, Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P

number theoryprimesA0052352 sources

declared openerdos:782

Erdős problem 782

number theoryN/A

declared solvederdos:783

Erdős problem 783

number theoryN/A3 sources

declared solvederdos:784

Erdős problem 784

number theoryN/A

declared open · formalizederdos:786

Erdos786.consecutivePrimesFrom 2 1 = {2, 3}

number theoryA143301 · possible2 sources

declared proved (Lean)erdos:793

Let

F(n)

be the largest

A\subseteq\{1,\dots,n\}

with

a\nmid bc

for distinct

a,b,c\in A

. Is

F(n)=\pi(n)+(C+o(1))\,n^{2/3}(\log n)^{-2}

for some constant

C

number theorypossible3 sources

declared provederdos:795

Erdős problem 795

number theorypossible

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

Erdős problem 820

number theoryA263647

declared open · formalizederdos:821

True ↔ ∀ ε > 0, {n | ↑(Erdos821.g n) > ↑n ^ (1 - ε)}.Infinite

number theoryA0141972 sources

declared proved · formalizederdos:822

True ↔ (Set.range fun n => n + n.totient).HasPosDensity

number theoryA121048 · A1550852 sources

declared provederdos:823

Erdős problem 823

number theoryN/A

declared openerdos:824

Erdős problem 824

number theorypossible

declared proved · formalized · $25erdos:825

True ↔ ∃ C, ∃ (_ : C > 0), ∀ (n : ℕ), ↑((ArithmeticFunction.sigma 1) n) > C * ↑n → ∃ s ⊆ n.properDivisors, n = s.sum id

number theoryA006037 · A3302442 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science