Skip to content

Problems · Vela Mathematics Program

Narrowed toopen ×irrationality ×Clear all

Problem ledger

13 problemsGraph view
declared open · formalizederdos:68
True ↔ Irrational (∑' (n : ℕ), 1 / (↑(n + 2).factorial - 1))
number theoryirrationalityA3313732 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 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 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 openerdos:265
Erdős problem 265
irrationalityN/A
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

Search problems.science

Find a Problem, Result, source, or page