Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×arithmetic progressions ×Clear all

Problem ledger

14 problemsGraph view
declared open · formalized · $5000erdos:3
True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k
number theoryadditive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources
declared proved · formalized · $1000erdos:139
∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)
additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources
declared open · formalizederdos:141
sorry ↔ ∀ k ≥ 3, ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s k
additive combinatoricsprimesarithmetic progressionsA0065602 sources
declared open · formalized · $10000erdos:142
∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry
additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources
declared open · formalizederdos:160
have lower_bound := sorry; (lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧ ∀ c > 0, ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) → ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound
additive combinatoricsarithmetic progressionspossible2 sources
declared disproved (Lean) · formalizederdos:194
False ↔ ∀ k ≥ 3, ∀ (r : ℝ → ℝ → Prop), IsStrictTotalOrder ℝ r → ∃ s, s.IsAPOfLength k ∧ (List.Pairwise r s ∨ List.Pairwise (flip r) s)
arithmetic progressionsN/A5 sources
declared open · formalizederdos:195
sorry = sSup {k | ∀ (f : ℤ ≃ ℤ), HasMonotoneAP (⇑f) k}
arithmetic progressionsN/A2 sources
declared open · formalizederdos:196
True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4
arithmetic progressionsN/A2 sources
declared open · formalizederdos:197
True ↔ ∃ A B, IsCompl A B ∧ (∃ f, ¬HasMonotoneAP (Subtype.val ∘ ⇑f) 3) ∧ ∃ g, ¬HasMonotoneAP (Subtype.val ∘ ⇑g) 3
arithmetic progressionsN/A2 sources
declared disproved (Lean) · formalizederdos:198
∀ (V : Type u_1) [inst : AddCommGroup V] [Module ℚ V], ∃ X, (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2
additive combinatoricssidon setsarithmetic progressionsN/A5 sources
declared disproved (Lean) · formalizederdos:199
False ↔ ∀ (A : Set ℝ), ThreeAPFree A → ∃ S, S.IsAPOfLength ⊤ ∧ S ⊆ Aᶜ
arithmetic progressionsN/A5 sources
declared open · formalizederdos:200
sorry ↔ (fun n => ↑(Erdos200.longestPrimeArithmeticProgressions n)) =o[Filter.atTop] fun n => Real.log ↑n
primesarithmetic progressionsA0051152 sources
declared proved · formalizederdos:219
∅ ∉ Erdos219.primeArithmeticProgressions
number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources
declared open · formalizederdos:272
Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos272.maxArithInterCard N)) sorry
additive combinatoricsarithmetic progressionspossible2 sources