Erdős problem 264
Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers such that converges and is not an irrationality sequence.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/264.lean¬Erdos264.IsIrrationalitySequence fun x => 2 ^ xSolvedStatement only, no proofformal statement reference
Proof manifests naming this Problem
- PLBY Lean proofs
ErdosProblems.Erdos264 - PLBY Lean proofs
ErdosProblems.Erdos264b
Reported activity
Reported by these sources. Not reviewed here.
AI building on literature
- Machine