Conjectures.io

Number theory

Erdős 770 - three

It is probably true that h n = 3 for infinitely many n.

References

  • [Er49d] Erdös, P. "On the strong law of large numbers." Transactions of the American Mathematical Society 67.1 (1949): 51-56.
  • [Ma66] Matsuyama, Noboru. "On the strong law of large numbers." Tohoku Mathematical Journal, Second Series 18.3 (1966): 259-269.

No one has attempted this yet.

Formal statement

Lean type

{n | Erdos770.h n = 3}.Infinite

What you must prove

import FormalConjectures.ErdosProblems.«770»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos770.erdos_770.variants.three" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/770.lean

Source type SHA-256
sha256:5cabe5b39227cd0b11b97d00e12b4cc741a1f9c65d23c26c3a1be36c7dcb5cf9
Task id
fc-379fc029-variants-three-b2b073631f-formalized-v1
Task commitment
sha256:d81de99617c5fac0f2f77013a8ba5c9ba92bea9f362587faed6e2c63f49d989d

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.