Number theory

Erdős problem 291 - shiu heuristic density zero

In particular, there should be infinitely many

n

, but the set of such

n

should have density zero. Unfortunately this heuristic is difficult to turn into a proof.

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«291»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos291.erdos_291.variants.shiu_heuristic_density_zero" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

Filter.Tendsto (fun N => ↑{n ∈ Finset.Icc 1 N | (Erdos291.a n).gcd (Erdos291.L n) = 1}.card / ↑N) Filter.atTop (nhds 0)

Original conjecture source: FormalConjectures/ErdosProblems/291.lean

Source type SHA-256: sha256:e2829c437fcad6fe1da19ab961ad301299f96cf725e6af3bfd671ecaeefcdf20
Task id: fc-v2-variants-shiu-heuristic-density-zero-b668e98f4bc900b0983f73d4-formalized
Task commitment: sha256:40ccfa70198a39ff29ad05cb462fd3561793b672a98425383f1cbf7eec443163

References

erdosproblems.com/291

[ErGr80, p.34] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
[Sh16] P. Shiu, The denominators of harmonic numbers. arXiv:1607.02863 (2016).
[WuYa22] Wu, Bing-Ling and Yan, Xiao-Hui, On the denominators of harmonic numbers. {IV}. C. R. Math. Acad. Sci. Paris (2022), 53--57.

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

import FormalConjectures.ErdosProblems.«291» import TaskSupport namespace Bounty theorem target : fcTypeOfName% "Erdos291.erdos_291.variants.shiu_heuristic_density_zero" := by sorry end Bounty