Mathematical statement
Let and be two sequences such that and
(a_n+1, b_n-f(a_n)) & \text{if } b_n \ge f(a_n) \\ (a_n, 3b_n+a_n+5) & \text{if } b_n < f(a_n) \end{cases}$$ where $f(x)=10\cdot 2^x-1$ for all non-negative integers $x$. Does there exist a positive integer $i$ such that $b_i = f(a_i)-1$? [BMO#5](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#5._1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE_(bbch)) is equivalent to asking whether the 6-state Turing machine [`1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE`](https://wiki.bbchallenge.org/wiki/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE) halts or not. There is presently no consensus on whether the machine halts or not, hence the problem is formulated using `answer(sorry) ↔`. The machine was discovered by [bbchallenge.org](bbchallenge.org) contributor mxdys on August 7th 2024. The correspondence between the machine's halting problem and the below reformulation has been proven in [Rocq](https://github.com/ccz181078/busycoq/blob/BB6/verify/1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE.v).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_5
Complete statement target, proof intentionally absentLean 4
theorem beaver_math_olympiad_problem_5 : answer(sorry) ↔ ∀ (a b f : ℕ → ℕ), ∀ᵉ (hf : f = fun x ↦ 10 * 2 ^ x - 1) (a_ini : a 0 = 0) (b_ini : b 0 = 5) (a_rec : ∀ n, a (n + 1) = if f (a n) ≤ b n then a n + 1 else a n) (b_rec : ∀ n, b (n+1) = if f (a n) ≤ b n then b n - f (a n) else 3 * b n + a n + 5), ∃ i, b i = f (a i) - 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