Number theory · Last catalog review 26 Jul 2026

Erdős Problem 912

Prove that there exists some

c>0

such that

h(n) \sim c \left(\frac{n}{\log n}\right)^{1/2}

n\to \infty

References

Published 6 May 2026Never attempted

Formal statement

Lean type

∃ c > 0, Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => c * (↑n / Real.log ↑n) ^ (1 / 2)

What you must prove

import FormalConjectures.ErdosProblems.«912»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos912.erdos_912" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/912.lean

Source type SHA-256: sha256:db634ec622da2c97ef6bccd55eebc0a3bd563529484de2686c2d9fa730bde50d
Task id: fc-e923379e-erdos912-erdos-912-cb11ec00a8-formalized-v1
Task commitment: sha256:03f2af980107e961941eea9432e7a4bab0709b2696265b9bb2fc9deff346e34b

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.