Number theory

Erdős 912 - tao

A heuristic of Tao using the Cramér model for the primes suggests this is true with

c=\sqrt{2\pi}

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

Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos912.h n)) fun n => √(2 * Real.pi) * (↑n / Real.log ↑n) ^ (1 / 2)

What you must prove

import FormalConjectures.ErdosProblems.«912»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/912.lean

Source type SHA-256: sha256:86a7121b84ed886e77186ebb259080e1fc8e9c8a77a4ae9f5d848c02ac9838db
Task id: fc-379fc029-variants-tao-9585d1a9d6-formalized-v1
Task commitment: sha256:4052f9d3347f589c52091c1f44c67fe969a302f4924708be08c775f5174bdb11

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.