Skip to content

Erdős problem 933

Start work

If n(n+1)=2k3lmn(n+1)=2^k3^lm, where (m,6)=1(m,6)=1, then is it true that lim sup⁡n→∞2k3lnlog⁡n=∞\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

933.lean

Retained formal statement1 of 3

If n(n+1)=2k3lmn(n+1)=2^k3^lm, where (m,6)=1(m,6)=1, then is it true that lim sup⁡n→∞2k3lnlog⁡n=∞\limsup_{n\to \infty} \frac{2^k3^l}{n\log n}=\infty?

FormalConjectures/ErdosProblems/933.leanErdos933.erdos_9331 lineExact file
True ↔ Filter.limsup (fun n => ↑↑(2 ^ Erdos933.k n * 3 ^ Erdos933.l n) / (↑↑n * ↑(Real.log ↑n))) Filter.atTop = ⊤
OpenStatement only, no proof