Beaver Math Olympiad (BMO)

formal-conjectures · other · ams-5 · ams-11 · ams-68

The Beaver Math Olympiad (BMO) is a set of mathematical reformulations of the halting/nonhalting
problem of specific Turing machines from all-0 tape. These problems came from studying small Busy
Beaver values. Some problems are open and have a conjectured answer, some are open and don't have a
conjectured answer, and, some are solved.

Among these problems is the Collatz-like *Antihydra* problem which is open and coming from a 6-state
Turing machine, and a testament to the difficulty of knowing the sixth Busy Beaver value.

For some BMO problem, the equivalence between the mathematical formulation and the corresponding
Turing machine non-termination has been formally proved in Rocq, we indicate it when done.

BMO#2

Antihydra is a sequence starting at 8, and iterating the function
$$H(n) = \left\lfloor \frac {3n}2 \right\rfloor.$$
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.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://bbchallenge.org
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://bbchallenge.org/antihydra
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://wiki.bbchallenge.org/wiki/Antihydra
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/Other/BeaverMathOlympiad.lean
Local target: Corpus.OtherBeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra
Source SHA-256: c42c35ef016e7ad8d0bcd4a872c40042440d04c6c385c7ba81713e6664874009
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record