Conjectures.io

Number theory

Erdős 1135

The Collatz conjecture states that for any positive integer nn, there exists a natural number mm such that the mm-th term of the sequence is 1.

References

  • [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
  • [La10] Lagarias, Jeffrey C., The {$3x+1$} problem: an overview. (2010), 3--29.
  • [La16] Lagarias, Jeffrey C., Erdős, Klarner, and the {$3x+1$} problem. Amer. Math. Monthly (2016), 753--776.
  • [La85] Lagarias, Jeffrey C., The {$3x+1$} problem and its generalizations. Amer. Math. Monthly (1985), 3--23.

No one has attempted this yet.

Formal statement

Lean type

∀ n > 0, ∃ m, CollatzConjecture.collatzStep^[m] n = 1

What you must prove

import FormalConjectures.ErdosProblems.«1135»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1135.erdos_1135" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1135.lean

Source type SHA-256
sha256:9ffc8897c27defc5d7172af89e2ab650c7e4404ff0e126a051d0dda128bd112d
Task id
fc-379fc029-erdos1135-erdos-1135-25ccb7b4a1-formalized-v1
Task commitment
sha256:7a0508602566d19605648115241fafabc1c2982ee4938904652051e5f0133c98

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.