Erdős problem 205
Is it true that all sufficiently large can be written as for some , where ? (Here is the number of prime divisors of counted with multiplicity.)
Sources
FormalConjectures/ErdosProblems/
205.lean
Retained formal statement
Is it true that all sufficiently large can be written as for some , where ? (Here is the number of prime divisors of counted with multiplicity.)
Barreto and Leeham, using ChatGPT and Aristotle, have proved a negative answer, which was quantified by Tao and Alexeev (see the comments): in fact there are infinitely many such that, for all with , has at least many prime factors.
False ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos205.IsRepresentable (fun m => Real.log (Real.log ↑m)) nSolvedStatement only, no proof