Conjectures.io

Number theory

Erdős 1095 - lower conjecture

Erdős, Lacampagne, and Selfridge [ELS93] write 'it is clear to every right-thinking person' that g(k)≥exp⁡(cklog⁡k)g(k)\geq\exp(c\frac{k}{\log k}) for some constant c>0c>0.

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

∃ c > 0, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(Erdos1095.g k) ≥ Real.exp (c * ↑k / Real.log ↑k)

What you must prove

import FormalConjectures.ErdosProblems.«1095»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1095.lean

Source type SHA-256
sha256:37d44d6c19d5ade926d4526f136139d92c93efb06d460b3208f456fd7e04f3f1
Task id
fc-379fc029-variants-lower-conjecture-a8643d7c9f-formalized-v1
Task commitment
sha256:47baaafa665f4abd15182d17b3342a789aa705b5a57eddf8e8817b863fdab718

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.