Vela Mathematics Program: problems

Narrowed tonumber theory ×Clear all

Problem ledger

576 problems · 11/12Number SourcesGraph view

declared proved (Lean) · formalizederdos:1000

True ↔ ∃ n, StrictMono n ∧ 0 < n 0 ∧ Filter.Tendsto (Erdos1000.phiAvg n) Filter.atTop (nhds 0)

number theorydiophantine approximationN/A5 sources

declared solvederdos:1001

Erdős problem 1001

number theorydiophantine approximationN/A

declared open · formalizederdos:1003

True ↔ {n | n.totient = (n + 1).totient}.Infinite

number theoryA0012742 sources

declared open · formalizederdos:1004

True ↔ ∀ c > 0, ∀ᶠ (x : ℕ) in Filter.atTop, ∃ n ≤ x, Erdos1004.IsDistinctTotientRun n ⌊Real.log ↑x ^ c⌋₊

number theorypossible3 sources

declared openerdos:1005

Erdős problem 1005

number theoryA386893

declared open · formalized · $10erdos:1052

sorry ↔ {n | Erdos1052.IsUnitaryPerfect n}.Finite

number theoryA0028272 sources

declared openerdos:1053

Erdős problem 1053

number theoryA007539

declared open · formalizederdos:1054

sorry ↔ (fun n => ↑(Erdos1054.f n)) =o[Filter.atTop] fun n => ↑n

number theorydivisorsA1674853 sources

declared open · formalizederdos:1055

∀ (r : ℕ+), {p | Nat.Prime p ∧ Erdos1055.IsOfClass r p}.Infinite

number theoryprimesA0051132 sources

declared open · formalizederdos:1056

True ↔ ∀ k ≥ 2, ∃ p, ∃ (_ : Nat.Prime p), ∃ boundaries, ∃ (_ : StrictMono boundaries), Erdos1056.AllModProdEqualsOne p boundaries

number theoryA0604273 sources

declared open · formalizederdos:1057

True ↔ Filter.Tendsto (fun x => Real.log (Erdos1057.carmichaelCounting x) / Real.log x) Filter.atTop (nhds 1)

number theoryA0069312 sources

declared provederdos:1058

Erdős problem 1058

number theoryN/A

declared open · formalizederdos:1059

Erdos1059.AllFactorialSubtractionsComposite 101

number theoryprimesA0641522 sources

declared open · formalizederdos:1060

∃ h, (h =o[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card ≤ ↑n ^ h n

number theoryA3271532 sources

declared open · formalizederdos:1061

For

S(x) = \#\{(a,b) : a + b \le x,\ \sigma(a) + \sigma(b) = \sigma(a+b)\}

, is

S(x) \sim cx

? The preprint claims

S(x)

grows faster than

x (\log x)^R

for every fixed

R

, ruling out the linear asymptotic.

number theoryA110177 · possible4 sources

declared open · formalizederdos:1062

(∃ l, Filter.Tendsto (fun n => ↑(Erdos1062.f n) / ↑n) Filter.atTop (nhds l) ∧ Irrational l) ↔ True

number theoryA0383723 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 proved · formalizederdos:1064

{n | n.totient > (n - n.totient).totient}.HasDensity 1

number theoryA051488 · A0514872 sources

declared open · formalizederdos:1065

True ↔ {p | ∃ q k, Nat.Prime p ∧ Nat.Prime q ∧ p = 2 ^ k * q + 1}.Infinite

number theoryA074781 · A3394652 sources

declared open · formalizederdos:1072

True ↔ {p | Nat.Prime p ∧ Erdos1072.f p = p - 1}.Infinite

number theoryA073944 · A072937 · A1545542 sources

declared open · formalizederdos:1073

True ↔ ∃ o, o =o[Filter.atTop] 1 ∧ ∀ (x : ℕ), Erdos1073.A x ≤ ↑x ^ o x

number theoryA2565192 sources

declared open · formalizederdos:1074

sorry ↔ ∃ c, Erdos1074.EHSNumbers.HasDensity c

number theoryA063980 · A0641642 sources

declared disprovederdos:1081

Erdős problem 1081

number theorypowerfulA076871 · A076872 · possible

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

declared proved · formalizederdos:1096

True ↔ ∃ ε > 0, ∀ (q : ℝ), 1 < q → q < 1 + ε → ∀ (x : ℕ → ℝ), StrictMono x → Set.range x = {x | ∃ S, ∑ i ∈ S, q ^ i = x} → Filter.Tendsto (fun k => x (k + 1) - x k) Filter.atTop (nhds 0)

number theoryN/A2 sources

declared open · formalizederdos:1097

False ↔ ∃ C > 0, ∀ (A : Finset ℤ), ↑(Erdos1097.CommonDifferencesThreeTermAP A).ncard ≤ C * ↑A.card ^ (3 / 2)

number theoryadditive combinatoricsN/A3 sources

declared provederdos:1099

Erdős problem 1099

number theorydivisorsN/A

declared openerdos:1100

Erdős problem 1100

number theorydivisorsA325864 · possible2 sources

declared open · formalizederdos:1101

Does there exist a good pairwise-coprime sequence

u_n

with

\sum 1/u_n < \infty

and polynomial growth? What if one only requires

u_n \le e^{o(n)}

number theoryN/A4 sources

declared solved (Lean) · formalizederdos:1102

∀ (A : ℕ → ℕ), StrictMono A → Erdos1102.HasPropertyP (Set.range A) → Filter.Tendsto (fun j => ↑(A j) / ↑j) Filter.atTop Filter.atTop

number theoryN/A5 sources

declared openerdos:1103

Erdős problem 1103

number theoryA392164

declared open · formalizederdos:1106

True ↔ Filter.Tendsto (fun n => (∏ i ∈ Finset.Icc 1 n, Erdos1106.p i).primeFactors.card) Filter.atTop Filter.atTop

number theoryA194259 · A1942602 sources

declared open · formalizederdos:1107

∀ r ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1107.SumOfRPowerful r n

number theorypowerfulA056828 · A392342 · A392343 · possible2 sources

declared open · formalizederdos:1108

True ↔ ∀ k ≥ 2, {a | a ∈ Erdos1108.FactorialSums ∧ ∃ m, m ^ k = a}.Finite

number theoryfactorialsA051761 · A115645 · A0254942 sources

declared openerdos:1109

Erdős problem 1109

number theoryA392164 · A392165

declared open · formalizederdos:1110

True ↔ ∀ (p q : ℕ), q < p → 2 ≤ q → p.Coprime q → ¬(p = 3 ∧ q = 2) → {n | n.Coprime (p * q) ∧ ¬Erdos1110.Representable p q n}.Infinite

number theorypossible2 sources

declared open · formalizederdos:1113

sorry ↔ ∃ k, k.IsSierpinskiNumber ∧ ¬Erdos1113.HasFinitePrimeCoveringSet k

number theorycovering systemsA0763362 sources

declared openerdos:1122

Erdős problem 1122

number theoryN/A

declared disproved (Lean) · £10erdos:1134

Erdős problem 1134

number theoryA1856613 sources

declared open · formalized · $500erdos:1135

∀ n > 0, ∃ m, CollatzConjecture.collatzStep^[m] n = 1

number theoryA006370 · A0089082 sources

declared proved (Lean) · formalizederdos:1136

True ↔ ∃ A, 1 / 3 < A.lowerDensity ∧ Erdos1136.AvoidsPowersOfTwo A

number theoryN/A5 sources

declared open · formalizederdos:1137

True ↔ Filter.Tendsto (fun x => ↑((Finset.range x).sup fun n => primeGap n * primeGap (n - 1)) / ↑((Finset.range x).sup primeGap) ^ 2) Filter.atTop (nhds 0)

number theoryprimesA083550 · A0052502 sources

declared disproved (Lean) · formalizederdos:1138

False ↔ ∀ C > 1, Asymptotics.IsEquivalent Erdos1138.snd_gt_half_fst (Erdos1138.primeCount_Ioc_mul_const C) fun x => match x with | (x, y) => C * ↑(Erdos1138.sup_primeGap x) / Real.log y

number theoryprimespossible6 sources

declared open · formalizederdos:1139

True ↔ Filter.limsup (fun k => (↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) - ↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) / ↑(Real.log (↑k + 1))) Filter.atTop = ⊤

number theoryprimesA037143 · A1010413 sources

declared disprovederdos:1140

Erdős problem 1140

number theorypossible

declared disproved (Lean) · formalizederdos:1141

False ↔ Infinite ↑{n | Erdos1141.Erdos1141Prop n}

number theoryprimesA2145836 sources

declared open · formalizederdos:1142

sorry ↔ Infinite ↑{n | Erdos1142.Erdos1142Prop n}

number theoryprimesA0396692 sources

declared openerdos:1143

Erdős problem 1143

number theoryprimesN/A2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science