Back to Problems

erdos_264.variants.ko_tao_pos

Specification

On the other hand, Kovač and Tao [KoTa24] do prove that for any function $F$ with $\lim_{n \to \infty} \frac{F(n + 1)}{F(n)} = \infty$ there exists such an irrationality sequence with $a_n \sim F(n)$. [KoTa24] Kovač, V. and Tao T., On several irrationality problems for Ahmes series. arXiv:2406.17593 (2024).

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem erdos_264.variants.ko_tao_pos {F : ℕ → ℕ}
    (hF : atTop.Tendsto (fun n ↦ (F (n + 1) : ℝ) / F n) atTop) :
    ∃ a : ℕ → ℕ, IsIrrationalitySequence a ∧ (fun n ↦ (a n : ℝ)) ~[atTop] fun n ↦ (F n : ℝ)
ID: ErdosProblems__264__erdos_264.variants.ko_tao_pos
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.