Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 82

F(n) / \log n \to \infty as n \to \infty

References

erdosproblems.com/82

Published 18 Jul 2026Never attempted

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-e923379e-erdos82-erdos-82-9a570bc88d-formalized-v1
Task commitment: sha256:0d5f58c8c421f76523aee7f13a486f28b9dc9ee08acab25f2f861632fb1506f5

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.