Number theory

Erdős 1074 - EHSNumbers one half

Regarding the first question, Hardy and Subbarao computed all EHS numbers up to

2^{10}

, and write "...if this trend conditions we expect [the limit] to be around 0.5, if it exists."

References

erdosproblems.com/1074

No one has attempted this yet.

Formal statement

Lean type

Erdos1074.EHSNumbers.HasDensity (1 / 2)

What you must prove

import FormalConjectures.ErdosProblems.«1074»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1074.erdos_1074.variants.EHSNumbers_one_half" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1074.lean

Source type SHA-256: sha256:ab7dd633c706410553805acc220e9409d13ef5746b39bf6fd142546f86097fe7
Task id: fc-379fc029-variants-ehsnumbers-one-half-ea93abd68f-formalized-v1
Task commitment: sha256:3e7e762ccc971964f32f8c11bbb6425864c494fc3f77d6b37dcb0df540f3ecfb

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.