Conjectures.io

Number theory

Erdős 414

Let h1(n)=h(n)h_1(n) = h(n) and hk(n)=h(hk−1(n))h_k(n) = h(h_{k-1}(n)). Is it true, for any m,nm,n, there exist ii and jj such that hi(m)=hj(n)h_i(m) = h_j(n)?

References

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ m > 0, ∀ n > 0, ∃ i j, Erdos414.h^[i] m = Erdos414.h^[j] n

What you must prove

import FormalConjectures.ErdosProblems.«414»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos414.erdos_414" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/414.lean

Source type SHA-256
sha256:f34e7a73bb00d956355b3dfaf8a9d2844d28196332c64b9aefc01342c404bd75
Task id
fc-379fc029-erdos414-erdos-414-9432727ecc-formalized-v1
Task commitment
sha256:747de99529ccf1de61336cbf0a6e1eb6e21c841ccf1a6bcf259fdc87aa2a8bae

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.