Vela Mathematics Program: problems

Narrowed toformalized ×covering systems ×Clear all

Problem ledger

declared verifiable · formalizederdos:7

Can there be a finite covering system of the integers with distinct moduli, all of which are odd and greater than

1

number theorycovering systemsN/A4 sources

declared solved (Lean) · formalizederdos:202

∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos202.f N) = ↑N * scaleL N ^ (-1 + o N)

covering systemsA3899756 sources

declared open · formalizederdos:203

True ↔ ∃ m, m.Coprime 6 ∧ ∀ (k l : ℕ), ¬Nat.Prime (2 ^ k * 3 ^ l * m + 1)

primescovering systemsN/A2 sources

declared disproved (Lean) · formalizederdos:204

False ↔ ∃ n a, have D := {d | d ∣ n ∧ d > 1}; (∀ (x : ℤ), ∃ d ∈ D, x ≡ a d [ZMOD ↑d]) ∧ ∀ d ∈ D, ∀ d' ∈ D, d ≠ d' → (∃ x, x ≡ a d [ZMOD ↑d] ∧ x ≡ a d' [ZMOD ↑d']) → d.gcd d' = 1

covering systemsN/A5 sources

declared open · formalizederdos:273

True ↔ ∃ c, ∀ (i : c.ι), ∃ p, Nat.Prime p ∧ 5 ≤ p ∧ c.moduli i = Ideal.span {↑(p - 1)}

number theorycovering systemsN/A2 sources

declared open · formalizederdos:274

sorry ↔ ∀ (G : Type u_1) [inst : Group G], 1 < ENat.card G → ∀ (ι : Type u_2) [inst_1 : Fintype ι] (P : Erdos274.Group.ExactCovering G ι), 1 < Fintype.card ι → ∃ i j, i ≠ j ∧ Cardinal.mk ↥(P.parts i) = Cardinal.mk ↥(P.parts j)

group theorycovering systemsN/A3 sources

declared proved (Lean) · formalizederdos:275

∀ (r : ℕ) (a : Fin r → ℤ) (n : Fin r → ℕ), (∃ k, ∀ x ∈ Set.Ico k (k + 2 ^ r), ∃ i, x ≡ a i [ZMOD ↑(n i)]) → ∀ (x : ℤ), ∃ i, x ≡ a i [ZMOD ↑(n i)]

number theorycovering systemsN/A5 sources

declared open · formalizederdos:276

True ↔ ∃ a, Erdos276.IsLucasSequence a ∧ (∀ (k : ℕ), (a k).Composite) ∧ ∀ n > 1, ∃ k, n.gcd (a k) = 1

number theorycovering systemsN/A2 sources

declared proved · formalizederdos:277

True ↔ ∀ (c : ℝ), ∃ n, ↑((ArithmeticFunction.sigma 1) n) > c * ↑n ∧ ∀ (m : StrictCoveringSystem ℤ), ∃ i, ↑n ∉ m.moduli i

number theorycovering systemsN/A2 sources

declared open · formalizederdos:279

True ↔ ∀ k ≥ 3, ∃ a N, (∀ (p : ℕ), Nat.Prime p → a p < p) ∧ ∀ n ≥ N, ∃ p, ∃ t ≥ k, Nat.Prime p ∧ n = a p + t * p

number theorycovering systemsprimesN/A2 sources

declared disproved (Lean) · formalizederdos:280

False ↔ ∀ (n a : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 1 ≤ i → a i < n i) → (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) → ¬Filter.Tendsto (fun k => ↑(Erdos280.uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)

number theorycovering systemsN/A5 sources

declared proved (Lean) · formalizederdos:281

True ↔ ∀ (n : ℕ → ℕ), StrictMono n → (∀ (i : ℕ), 0 < n i) → (∀ (a : Erdos281.ResidueChoice n), (Erdos281.avoidAll n a).HasIntDensity 0) → ∀ (ε : ℝ), 0 < ε → ∃ k, ∀ (a : Erdos281.ResidueChoice n), ∃ d, (Erdos281.avoidPrefix n a k).HasIntDensity d ∧ d < ε

number theorycovering systemsN/A7 sources

declared open · formalizederdos:1113

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

number theorycovering systemsA0763362 sources

declared open · formalizederdos:1188

Estimate the number

F(x)

of minimal distinct covering systems whose moduli all lie in

[1, x]

. The candidate proof gives

\log\log F(x)/\log x \to 1

, i.e.

F(x) = \exp(x^{1+o(1)})

number theorycovering systemspossible4 sources

declared solved (Lean) · formalizederdos:1190

∀ (ε : ℝ), 0 < ε → ∀ᶠ (m : ℕ) in Filter.atTop, scaleL m ^ (-1 - ε) < Erdos1190.eps m ∧ Erdos1190.eps m < scaleL m ^ (-1 + ε)

number theorycovering systemspossible6 sources

Problems · Vela Mathematics Program

Problem ledger