Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×irrationality ×Clear all

Problem ledger

18 problemsGraph view
declared open · formalizederdos:68
True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1))
number theoryirrationalityA3313732 sources
declared proved · formalizederdos:69
Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.cardDistinctFactors (n + 2)) / 2 ^ (n + 2))
number theoryirrationalityA2621532 sources
declared open · formalizederdos:247
True ↔ ∀ (n : ℕ → ℕ), StrictMono n → Filter.limsup (fun k => ↑(n k) / ↑k.succ) Filter.atTop = ⊤ → Transcendental ℚ (∑' (k : ℕ), 1 / 2 ^ n k)
number theoryirrationalityN/A2 sources
declared open · formalizederdos:249
True ↔ Irrational (∑' (n : ℕ), ↑n.totient / 2 ^ n)
number theoryirrationalityA2569362 sources
declared proved · formalizederdos:250
(∀ (x : ℝ), HasSum (fun n => ↑((ArithmeticFunction.sigma 1) n) / 2 ^ n) x → Irrational x) ↔ True
number theoryirrationalityA0667662 sources
declared open · formalizederdos:251
True ↔ Irrational (∑' (n : ℕ), ↑(Nat.nth Nat.Prime n) / 2 ^ n)
number theoryirrationalityA0989903 sources
declared open · formalizederdos:252
True ↔ ∀ k ≥ 1, Irrational (Erdos252.erdos_252_sum k)
number theoryirrationalityA227988 · A227989 · A307036 · A359060 · possible2 sources
declared open · formalizederdos:257
True ↔ ∀ (A : Set ℕ), A.Infinite → Irrational (∑' (n : ↑A), 1 / (2 ^ ↑n - 1))
irrationalityN/A2 sources
declared proved (Lean) · formalizederdos:258
True ↔ ∀ (a : ℕ → ℕ), (∀ (n : ℕ), 2 ≤ a n) → Filter.Tendsto a Filter.atTop Filter.atTop → Irrational (∑' (n : ℕ), ↑(n + 1).divisors.card / ↑(∏ i ∈ Finset.Icc 1 (n + 1), a i))
irrationalityN/A6 sources
declared proved (Lean) · formalizederdos:259
Irrational (∑' (n : ℕ), ↑(ArithmeticFunction.moebius n) ^ 2 * ↑n / 2 ^ n)
irrationalityA3711345 sources
declared open · formalizederdos:260
sorry ↔ ∀ (a : ℕ → ℤ) (s : ℝ), StrictMono a → Filter.Tendsto (fun n => ↑(a n) / ↑n) Filter.atTop Filter.atTop → HasSum (fun n => ↑(a n) / 2 ^ a n) s → Irrational s
irrationalityN/A2 sources
declared open · formalizederdos:263
sorry ↔ Erdos263.IsIrrationalitySequence fun n => 2 ^ 2 ^ n
irrationalityN/A3 sources
declared open · formalizederdos:264
¬Erdos264.IsIrrationalitySequence fun x => 2 ^ x
irrationalityN/A4 sources
declared disproved · formalizederdos:266
¬∀ (a : ℕ → ℕ), ((∀ (n : ℕ), a n ≥ 1) ∧ Summable fun x => 1 / ↑(a x)) → ∃ t ≥ 1, Irrational (∑' (n : ℕ), 1 / (↑(a n) + ↑t))
irrationalityN/A2 sources
declared open · formalizederdos:267
If n1<n2<⋯n_1 < n_2 < \cdots with nk+1/nk≥c>1n_{k+1}/n_k \ge c > 1, must ∑k1/Fnk\sum_k 1/F_{n_k} be irrational? The proposed proof closes the range 1<c<21 < c < 2 left open by earlier criteria.
irrationalityN/A4 sources
declared open · formalizederdos:269
∀ (P : Set ℕ), (∀ p ∈ P, Nat.Prime p) → P.Infinite → Irrational (Erdos269.series P)
irrationalityN/A2 sources
declared open · formalizederdos:1049
True ↔ ∀ t > 1, Irrational (∑' (n : ℕ+), 1 / (↑t ^ ↑n - 1))
irrationalityN/A2 sources
declared proved (Lean) · formalizederdos:1051
True ↔ ∀ (a : ℕ → ℤ), StrictMono a → Erdos1051.GrowthCondition a → Irrational (Erdos1051.ErdosSeries a)
irrationalityN/A6 sources

Search problems.science

Find a Problem, Result, source, or page