Conjectures.io

Combinatorics

Erdős 82

F(n)/log⁡n→∞asn→∞F(n) / \log n \to \infty as n \to \infty

References

No one has attempted this yet.

Formal statement

Lean type

Filter.Tendsto (fun n => ↑(Erdos82.F n) / Real.log ↑n) Filter.atTop Filter.atTop

What you must prove

import FormalConjectures.ErdosProblems.«82»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos82.erdos_82" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/82.lean

Source type SHA-256
sha256:cf3932e65018cf1da8fdceb468deafb47936cf7bfb3d85d4e8ba9b26c7475331
Task id
fc-379fc029-erdos82-erdos-82-389c60f7ba-formalized-v1
Task commitment
sha256:86d1d32693f6e1fd64534d762d3baa44ea9e286d9163c51186289fec77a96e0b

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.