Vela Mathematics Program: problems

Problem ledger

1,217 problems · 22/25Number SourcesGraph view

declared proved (Lean) · formalizederdos:1051

True ↔ ∀ (a : ℕ → ℤ), StrictMono a → Erdos1051.GrowthCondition a → Irrational (Erdos1051.ErdosSeries a)

irrationalityN/A6 sources

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

Erdős problem 1066

graph theoryplanar graphspossible

declared disproved (Lean) · formalizederdos:1067

False ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ H, H.coe.chromaticCardinal = Cardinal.aleph 1 ∧ H.coe.InfinitelyConnected

graph theoryset theoryN/A5 sources

declared open · formalizederdos:1068

True ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ s, s.Countable ∧ (SimpleGraph.induce s G).InfinitelyConnected

graph theoryset theorychromatic numberN/A2 sources

declared solvederdos:1069

Erdős problem 1069

geometrypossible

declared openerdos:1070

Erdős problem 1070

geometrypossible2 sources

declared proved (Lean) · formalizederdos:1071

True ↔ ∃ S, Maximal (fun T => (∀ seg ∈ T, dist seg.1 seg.2 = 1 ∧ seg.1.ofLp 0 ∈ Set.Icc 0 1 ∧ seg.1.ofLp 1 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 0 ∈ Set.Icc 0 1 ∧ seg.2.ofLp 1 ∈ Set.Icc 0 1) ∧ (↑T).Pairwise Erdos1071.SegmentsDisjoint) S

geometryN/A5 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 openerdos:1075

Erdős problem 1075

hypergraphsN/A

declared provederdos:1076

Erdős problem 1076

hypergraphspossible

declared disproved · formalizederdos:1077

False ↔ ∀ ε > 0, ε < 1 → ∀ α > 0, α < 1 → ∀ᶠ (D : ℝ) in Filter.atTop, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), ↑G.edgeSet.ncard > ↑n ^ (1 + α) → ∃ H, H.coe.IsBalanced D ∧ ↑H.verts.ncard > ↑n ^ (1 - α) ∧ ↑H.edgeSet.ncard > ε * ↑H.verts.ncard ^ (1 + α)

graph theoryN/A2 sources

declared provederdos:1078

Erdős problem 1078

graph theoryN/A

declared solvederdos:1079

Erdős problem 1079

graph theoryturan numberN/A

declared disproved (Lean) · formalizederdos:1080

False ↔ ∃ c > 0, ∀ (V : Type) [inst : Fintype V] [Nonempty V] (G : SimpleGraph V) (X Y : Set V), Erdos1080.IsBipartition G X Y → X.ncard = ⌊↑(Fintype.card V) ^ (2 / 3)⌋₊ → ↑G.edgeSet.ncard ≥ c * ↑(Fintype.card V) → ∃ v walk, walk.IsCycle ∧ walk.length = 6

graph theorypossible5 sources

declared disprovederdos:1081

Erdős problem 1081

number theorypowerfulA076871 · A076872 · possible

declared falsifiable · formalizederdos:1082

True ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear ↑A → A.card / 2 ≤ EuclideanGeometry.distinctDistances A

geometrydistancespossible3 sources

declared openerdos:1083

Erdős problem 1083

geometrydistancesA186704 · possible

declared open · formalizederdos:1084

∀ {n : ℕ}, n ≠ 0 → Erdos1084.f 2 n < 3 * n

geometrydistancesA045945 · possible3 sources

declared open · formalizederdos:1085

∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (1 + c / Real.log (Real.log ↑n)) < ↑(Erdos1085.f 2 n)

geometrydistancesA186705 · possible2 sources

declared openerdos:1086

Erdős problem 1086

geometrydistancespossible

declared openerdos:1087

Erdős problem 1087

geometrydistancespossible

declared openerdos:1088

Erdős problem 1088

geometrypossible

declared solvederdos:1089

Erdős problem 1089

geometrydistancespossible3 sources

declared proved (Lean) · formalizederdos:1090

True ↔ ∀ (k : ℕ), 3 ≤ k → ∃ A, ∀ (C : ↥A → Fin 2), ∃ S, ∃ (hSA : S ⊆ A), Collinear ℝ ↑S ∧ S.card ≥ k ∧ (∀ y ∈ A, y ∈ affineSpan ℝ ↑S → y ∈ S) ∧ ∃ c, ∀ (x : Fin 2 → ℝ) (hx : x ∈ S), C ⟨x, ⋯⟩ = c

geometryramsey theoryN/A5 sources

declared solvederdos:1091

Erdős problem 1091

geometrychromatic numberN/A3 sources

declared disproved · formalizederdos:1092

False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)

geometrychromatic numberN/A5 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

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 proved (Lean) · formalizederdos:1098

True ↔ ∀ (G : Type u_1) [inst : Group G], (∀ (s : Set G), (Erdos1098.nonCommutingGraph G).IsClique s → s.Finite) → ∃ n, ∀ (s : Finset G), (Erdos1098.nonCommutingGraph G).IsClique ↑s → s.card ≤ n

group theoryN/A5 sources

declared provederdos:1099

Erdős problem 1099

number theorydivisorsN/A

declared openerdos:1100

Erdős problem 1100

number theorydivisorsA325864 · possible2 sources

Problems · Vela Mathematics Program

Problem ledger