FormalConjectures/Other/BeaverMathOlympiad.lean

GitHub source file

7 declarations, 7 contain sorry, 0 declared as axioms

1. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_1 Documented declaration: beaver_math_olympiad_problem_1 sorry line 71 source

   Source documentation

   BMO#1

   Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be two sequences such that $(a_1, b_1) = (1, 2)$ and

   $$(a_{n+1}, b_{n+1}) = \begin{cases} (a_n-b_n, 4b_n+2) & \text{if }a_n \ge b_n \cr (2a_n+1, b_n-a_n) & \text{if }a_n < b_n \end{cases}$$

   for all positive integers $n$. Does there exist a positive integer $i$ such that $a_i = b_i$?

   The first 10 values of $(a_n, b_n)$ are $(1, 2), (3, 1), (2, 6), (5, 4), (1, 18), (3, 17), (7, 14), (15, 7), (8, 30), (17, 22)$.

   BMO#1 is equivalent to asking whether the 6-state Turing machine 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE 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 contributor Jason Yuen on June 25th 2024.

   L4DEL explanation

   BMO#1) Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be two sequences such that $(a_1, b_1) = (1, 2)$ and $$(a_{n+1}, b_{n+1}) = \begin{cases} (a_n-b_n, 4b_n+2) & \text{if }a_n \ge b_n \cr (2a_n+1, b_n-a_n) & \text{if }a_n < b_n \end{cases}$$ for all positive integers $n$. Does there exist a positive integer $i$ such that $a_i = b_i$? The first 10 values of $(a_n, b_n)$ are $(1, 2), (3, 1), (2, 6), (5, 4), (1, 18), (3, 17), (7, 14), (15, 7), (8, 30), (17, 22)$. BMO#1) is equivalent to asking whether the 6-state Turing machine 1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE 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 contributor Jason Yuen on June 25th 2024.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, True, Nat, Eq, OfNat.ofNat, HAdd.hAdd, ite, LE.le, HSub.hSub, HMul.hMul, Exists

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem beaver_math_olympiad_problem_1 :
       answer(sorry) ↔ ∀ᵉ (a : ℕ → ℕ) (b : ℕ → ℕ)
       (a_ini : a 0 = 1)
       (a_rec : ∀ n, a (n + 1) = if b n ≤ a n then a n - b n else 2 * a n + 1)
       (b_ini : b 0 = 2)
       (b_rec : ∀ n, b (n + 1) = if b n ≤ a n then 4 * b n + 2 else b n - a n),
       ∃ i, a i = b i := by
   …

2. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra BMO#2 Antihydra is a sequence starting at 8, and iterating the function sorry line 98 source

   Source documentation

   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.

   L4DEL explanation

   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.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Nat, Int, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HMul.hMul, ite, HMod.hMod, HSub.hSub, GE.ge

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   30 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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
   …

3. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_2_antihydra.variants.set BMO#2 formulation variant Alternative statement of beaver_math_olympiad_problem_2_antihydra using set size comparison instead of a recurrent sequence b sorry line 114 source

   Source documentation

   BMO#2 formulation variant

   Alternative statement of beaver_math_olympiad_problem_2_antihydra using set size comparison instead of a recurrent sequence b.

   L4DEL explanation

   BMO#2 formulation variant Alternative statement of beaver_math_olympiad_problem_2_antihydra using set size comparison instead of a recurrent sequence b.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Nat, Eq, OfNat.ofNat, HAdd.hAdd, HDiv.hDiv, HMul.hMul, LE.le, Finset.card, Finset.filter, Odd, Finset.Ico, Even

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem beaver_math_olympiad_problem_2_antihydra.variants.set
       (a : ℕ → ℕ) (a_ini : a 0 = 8)
       (a_rec : ∀ n, a (n + 1) = (3 * a n) / 2) (n : ℕ) :
       ((Finset.Ico 0 n).filter fun x ↦ Odd (a x)).card ≤
         2 * ((Finset.Ico 0 n).filter fun x ↦ Even (a x)).card := by
   …

4. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_3 sorry line 143 source

   depends on sorry what this means

   Statement uses: Nat, Eq, OfNat.ofNat, HAdd.hAdd, HSub.hSub, HPow.hPow, padicValNat, Not, Exists

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

5. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_4 sorry line 174 source

   depends on sorry what this means

   Statement uses: Nat, Eq, OfNat.ofNat, HAdd.hAdd, ite, HMod.hMod, HDiv.hDiv, HPow.hPow, HSub.hSub, Not, Exists

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

6. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_5 Documented declaration: beaver_math_olympiad_problem_5 sorry line 209 source

   Source documentation

   BMO#5

   Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be two sequences such that $(a_1, b_1) = (0, 5)$ and

   $$(a_{n+1}, b_{n+1}) = \begin{cases} (a_n+1, b_n-f(a_n)) & \text{if } b_n \ge f(a_n) \cr (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 is equivalent to asking whether the 6-state Turing machine 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 contributor mxdys on August 7th 2024.

   The correspondence between the machine's halting problem and the below reformulation has been proven in Rocq.

   L4DEL explanation

   BMO#5) Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be two sequences such that $(a_1, b_1) = (0, 5)$ and $$(a_{n+1}, b_{n+1}) = \begin{cases} (a_n+1, b_n-f(a_n)) & \text{if } b_n \ge f(a_n) \cr (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) is equivalent to asking whether the 6-state Turing machine 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 contributor mxdys on August 7th 2024. The correspondence between the machine's halting problem and the below reformulation has been proven in Rocq.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, True, Nat, Eq, HSub.hSub, HMul.hMul, OfNat.ofNat, HPow.hPow, HAdd.hAdd, ite, LE.le, Exists

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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
   …

7. theorem BeaverMathOlympiad.beaver_math_olympiad_problem_8 Documented declaration: beaver_math_olympiad_problem_8 sorry line 237 source

   Source documentation

   BMO#8

   Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be two sequences such that $(a_1, b_1) = (10, 12)$ and

   $$(a_{n+1}, b_{n+1}) = \begin{cases} (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 \cr (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 is equivalent to asking whether the 6-state Turing machine 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) ↔.

   L4DEL explanation

   BMO#8) Let $(a_n)_{n \ge 1}$ and $(b_n)_{n \ge 1}$ be two sequences such that $(a_1, b_1) = (10, 12)$ and $$(a_{n+1}, b_{n+1}) = \begin{cases} (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 \cr (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) is equivalent to asking whether the 6-state Turing machine 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) ↔.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, True, Nat, Int, Eq, OfNat.ofNat, HAdd.hAdd, ite, LT.lt, HDiv.hDiv, HSub.hSub, HMul.hMul, Exists

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   26 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   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
   …