Number theory

Erdős 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

erdosproblems.com/912

Er82c Erdős, P., Miscellaneous problems in number theory. Congr. Numer. (1982), 25-45.

No one has attempted this yet.

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-379fc029-erdos912-erdos-912-422479db2d-formalized-v1
Task commitment: sha256:feb3b28e7e6b522081d19f3565cbd6b1c929b88637f3e35c66abb5e171be3f0b

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.