Mathematical statement
Antihydra is a sequence starting at 8, and iterating the function The conjecture states that the cumulative number of odd values in this sequence is never more than twice the cumulative number of even values. It is a relatively new open problem with, so it might be solvable, although seems quite hard because of its Collatz-like flavor. The underlying Collatz-like map has been studied independently in the past, see doi:10.1017/S0017089508004655 (Corollary 4).
It is equivalent to non-termination of the 1RB1RA_0LC1LE_1LD1LC_1LA0LB_1LF1RE_---0RA 6-state Turing machine (from all-0 tape). Note that the conjecture
that the machine does not halt is based on a probabilistic argument.
This machine and its mathematical reformulations were found by bbchallenge.org contributors mxdys and Rachel Hunter on June 28th 2024.
Statement source: Other statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
beaver_math_olympiad_problem_2_antihydra
theorem beaver_math_olympiad_problem_2_antihydra (a : ℕ → ℕ) (b : ℕ → ℤ) (a_ini : a 0 = 8) (a_rec : ∀ n, a (n + 1) = (3 * a n) / 2) (b_ini : b 0 = 0) (b_rec : ∀ n, b (n + 1) = if a n % 2 = 0 then b n + 2 else b n - 1) : ∀ n, b n ≥ 0 := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References