Mathematical statement
Let and be two sequences such that and
(a_n - \lfloor b_n/2 \rfloor - 3, 3 \lfloor (b_n+1)/2 \rfloor + 6) & \text{if } a_n > \lfloor b_n/2 \rfloor \\ (3 a_n + 5, b_n - 2 a_n) & \text{if } a_n \le \lfloor b_n/2 \rfloor \end{cases}$$ for all positive integers $n$. Does there exist a positive integer $i$ such that $a_i = \lfloor b_i/2 \rfloor + 1$? [BMO#8](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#8._1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA_(bbch)) is equivalent to asking whether the 6-state Turing machine [`1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA`](https://wiki.bbchallenge.org/wiki/1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA) halts or not. There is presently no consensus on whether the machine halts or not, hence the problem is formulated using `answer(sorry) ↔`.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_8
Complete statement target, proof intentionally absentLean 4
theorem beaver_math_olympiad_problem_8 : answer(sorry) ↔ ∀ᵉ (a : ℕ → ℕ) (b : ℕ → ℕ) (a_ini : a 0 = 10) (a_rec : ∀ n, a (n + 1) = if b n / 2 < a n then a n - b n / 2 - 3 else 3 * a n + 5) (b_ini : b 0 = 12) (b_rec : ∀ n, b (n + 1) = if b n / 2 < a n then 3 * ((b n + 1) / 2) + 6 else b n - 2 * a n), ∃ i, a i = b i / 2 + 1 := 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