Conjectures.io

Number theory

Erdős 1095 - log isTheta

Sorenson, Sorenson, and Webster [SSWE20] give heuristic evidence that log⁡g(k)≍klog⁡k\log g(k) \asymp \frac{k}{\log k}.

References

  • [EES74] Ecklund, Jr., E. F. and Erd\H{o}s, P. and Selfridge, J. L., A new function associated with the prime factors of {$(\sp{n}\sb{k})$}. Math. Comp. (1974), 647--649.
  • [ELS93] Erdős, P. and Lacampagne, C. B. and Selfridge, J. L., Estimates of the least prime factor of a binomial coefficient. Math. Comp. (1993), 215--224.
  • [GrRa96] Granville, Andrew and Ramaré, Olivier, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients. Mathematika (1996), 73--107.
  • [Ko99b] Konyagin, S. V., Estimates of the least prime factor of a binomial coefficient. Mathematika (1999), 41--55.
  • [SSW20] Sorenson, Brianna and Sorenson, Jonathan and Webster, Jonathan, An algorithm and estimates for the {E}rdős-{S}elfridge function. (2020), 371--385.

No one has attempted this yet.

Formal statement

Lean type

(fun k => Real.log ↑(Erdos1095.g k)) =Θ[Filter.atTop] fun k => ↑k / Real.log ↑k

What you must prove

import FormalConjectures.ErdosProblems.«1095»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1095.erdos_1095.variants.log_isTheta" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1095.lean

Source type SHA-256
sha256:8c6b1dff26369eee096133e410b35d7a3fcf94d748f974cf22d47f61eb69f601
Task id
fc-379fc029-variants-log-istheta-c279801145-formalized-v1
Task commitment
sha256:6c96066fadb8bca54a721bdf1959608f4619236d526bb3f7f06a823876bdc185

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.