All open problems
Source labels openChecked July 26, 2026
Erdős Problem 264: Ii
Is an example of an irrationality sequence?
Mathematical statement
Is an example of an irrationality sequence?
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_264.parts.ii
Complete statement target, proof intentionally absentLean 4
theorem erdos_264.parts.ii : answer(sorry) ↔ IsIrrationalitySequence Nat.factorial := by sorry /--One example is $2^{2^n}$.-/@[category research solved, AMS 11]theorem erdos_264.variants.example : IsIrrationalitySequence (fun n ↦ 2 ^ (2 ^ n)) := by sorry /--Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers$a_n$ such that $\sum \frac{1}{a_n}$ converges and$$ \liminf_{n \to \infty} (a_n^2 \sum_{k > n} \frac{1}{a_k^2}) > 0$$is not an irrationality sequence. [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).-/@[category research solved, AMS 11]theorem erdos_264.variants.ko_tao_neg {a : ℕ → ℕ} (h₁ : StrictMono a) (h₂ : 0 ∉ Set.range a) (h₃ : Summable ((1 : ℝ) / a ·)) (h₄ : 0 < atTop.liminf fun n ↦ a n ^ 2 * ∑' k : Set.Ioi n, (1 : ℝ) / a k ^ 2) : ¬IsIrrationalitySequence a := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References