Number theory

Erdős 945

Is it true that

F(x) \leq (\log x)^{O(1)}

References

erdosproblems.com/945

[ErMi52] Erdős, P. and Mirsky, L., The distribution of values of the divisor function {$d(n)$}. Proc. London Math. Soc. (3) (1952), 257--271.

No one has attempted this yet.

Formal statement

Lean type

True ↔ Erdos945.Erdos945Prop

What you must prove

import FormalConjectures.ErdosProblems.«945»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos945.erdos_945" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/945.lean

Source type SHA-256: sha256:eab5b8eae8550d0644aee25494ee33af0be37757c4e9f126f14b711ae959841a
Task id: fc-379fc029-erdos945-erdos-945-40715e749d-formalized-v1
Task commitment: sha256:e06412f1578a0680a7ac6785251c2613f4cc549c59aa12745ff36375c6104d0c

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.