Beaver Math Olympiad: Difference between revisions
RobinCodes (talk | contribs) →Solved problems: Add links to Discord for the formalised solution |
→6. 1RB1LA_1LC0RE_1LF1LD_0RB0LA_1RC1RE_---0LD (bbch): rename section to Space Needle like how BMO 2 is "Hydra and Antihydra" |
||
| (7 intermediate revisions by 4 users not shown) | |||
| Line 2: | Line 2: | ||
The purpose of the BMO is twofold. First, statements where non-essential details (related to tape encoding, number of steps, etc.) are discarded are more suitable to be shared with mathematicians who perhaps are able to help. Second, it's a way to jokingly highlight how a hard question could appear deceptively simple. | The purpose of the BMO is twofold. First, statements where non-essential details (related to tape encoding, number of steps, etc.) are discarded are more suitable to be shared with mathematicians who perhaps are able to help. Second, it's a way to jokingly highlight how a hard question could appear deceptively simple. | ||
BMO problems have been formalized in Lean and added to the DeepMind formal-conjectures database ([https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Other/BeaverMathOlympiad.lean Github]). | |||
== Unsolved problems == | == Unsolved problems == | ||
| Line 38: | Line 40: | ||
Does there exist a positive integer <math>i</math> such that <math>b_i = f(a_i)-1</math>? | Does there exist a positive integer <math>i</math> such that <math>b_i = f(a_i)-1</math>? | ||
=== 6. | === 6. [[Space Needle]] === | ||
Let <math>f(b) = b + k + 3a</math>, where <math>k</math> and <math>a</math> are non-negative integers satisfying <math>b = (2a+1)\cdot 2^k</math>. | Let <math>f(b) = b + k + 3a</math>, where <math>k</math> and <math>a</math> are non-negative integers satisfying <math>b = (2a+1)\cdot 2^k</math>. | ||
Now consider the iterated application of the function <math>f^{n+1}(b) = f(f^n(b))</math>, <math>f^0(b)=b</math>. Does there exist a non-negative integer <math>n</math> such that <math>f^n(6)</math> equals a power of 2? | Now consider the iterated application of the function <math>f^{n+1}(b) = f(f^n(b))</math>, <math>f^0(b)=b</math>. Does there exist a non-negative integer <math>n</math> such that <math>f^n(6)</math> equals a power of 2? | ||
=== 8. {{TM|1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA|undecided}} === | |||
Let <math>(a_n)_{n \ge 1}</math> and <math>(b_n)_{n \ge 1}</math> be two sequences such that <math>(a_1, b_1) = (10, 12)</math> and | |||
<math display="block">(a_{n+1}, b_{n+1}) = \begin{cases} | |||
(a_n-\left\lfloor\frac{b_n}{2}\right\rfloor-3, 3\left\lfloor\frac{b_n+1}{2}\right\rfloor+6) & \text{if }a_n > \left\lfloor\frac{b_n}{2}\right\rfloor \\ | |||
(3a_n+5, b_n-2a_n) & \text{if }a_n \le \left\lfloor\frac{b_n}{2}\right\rfloor | |||
\end{cases}</math> | |||
for all positive integers <math>n</math>. Does there exist a positive integer <math>i</math> such that <math>a_n = \left\lfloor \frac{b_n}{2} \right\rfloor + 1</math>? | |||
== Solved problems == | == Solved problems == | ||
Latest revision as of 17:14, 28 April 2026
Beaver Mathematical Olympiad (BMO) is an attempt to re-formulate the halting problem for some particular Turing machines as a mathematical problem in a style suitable for a hypothetical math olympiad.
The purpose of the BMO is twofold. First, statements where non-essential details (related to tape encoding, number of steps, etc.) are discarded are more suitable to be shared with mathematicians who perhaps are able to help. Second, it's a way to jokingly highlight how a hard question could appear deceptively simple.
BMO problems have been formalized in Lean and added to the DeepMind formal-conjectures database (Github).
Unsolved problems
1. 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE (bbch)
Let and be two sequences such that and
for all positive integers . Does there exist a positive integer such that ?
The first 10 values of are .
2. Hydra and Antihydra
Let be a sequence such that for all non-negative integers .
- If , does there exist a non-negative integer such that the list of numbers have more than twice as many even numbers as odd numbers? (Hydra)
- If , does there exist a non-negative integer such that the list of numbers have more than twice as many odd numbers as even numbers? (Antihydra)
5. 1RB0LD_1LC0RA_1RA1LB_1LA1LE_1RF0LC_---0RE (bbch)
Let and be two sequences such that and
where for all non-negative integers .
Does there exist a positive integer such that ?
6. Space Needle
Let , where and are non-negative integers satisfying .
Now consider the iterated application of the function , . Does there exist a non-negative integer such that equals a power of 2?
8. 1RB0LD_0RC1RB_0RD0RA_1LE0RD_1LF---_0LA1LA (bbch)
Let and be two sequences such that and
for all positive integers . Does there exist a positive integer such that ?
Solved problems
3. 1RB0RB3LA4LA2RA_2LB3RA---3RA4RB (bbch) and 1RB1RB3LA4LA2RA_2LB3RA---3RA4RB (bbch)
Let be the largest integer such that divides . Let be a sequence such that
for all non-negative integers . Is there an integer such that for some positive integer ?
Link to Discord discussion: https://discord.com/channels/960643023006490684/1084047886494470185/1252634913220591728
Formalised solution: Initial announcement, Lean proof, LLM-translated Rocq proof, Proof of closure of existing mid-level rules.
4. 1RB3RB---1LB0LA_2LA4RA3LA4RB1LB (bbch)
Bonnie the beaver was bored, so she tried to construct a sequence of integers . She first defined , then defined depending on and using the following rules:
- If , then .
- If , then .
With these two rules alone, Bonnie calculates the first few terms in the sequence: . At this point, Bonnie plans to continue writing terms until a term becomes . If Bonnie sticks to her plan, will she ever finish?
How to guess the closed-form solution: Firstly, notice that . Secondly, calculate the error term . The error term appears to have a period of 4. This leads to the following guess:
This closed-form solution can be proven correct by induction. Unfortunately, the induction may require a lot of tedious calculations.
For all , we have and . Therefore, Bonnie will never finish.
7. 1RB1RF_1RC0RA_1LD1RC_1LE0LE_0RA0LD_0RB--- (bbch)
Let be the largest integer such that divides .
Let .
Now consider the iterated application of the function , .
Let be a sequence such that and for all non-negative integers .
Does there exist a non-negative integer such that is even?
(for simplicity, this question is slightly stronger than the halting problem of this TM)
Link to Discord discussion: https://discord.com/channels/960643023006490684/1421782442213376000/1431483206208852001
Practice Problems
Problems that are not BMO-level, but provide counter-examples to certain probvious intuition: