Questions, not proof records
Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.
sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.The negation of Finite.Equation677_implies_Equation255.
Probably this is true. It would be a stronger form of
Equation677_not_implies_Equation255.
Discussion thread here: https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/FINITE.3A.20677.20-.3E.20255
The negation of Finite.Equation677_not_implies_Equation255.
Probably this is false.
Let and be two sequences such that and
(a_n-b_n, 4b_n+2) & \text{if }a_n \ge b_n \\ (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](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#1._1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE_(bbch)) is equivalent to asking whether the 6-state Turing machine [`1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE`](https://wiki.bbchallenge.org/wiki/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](bbchallenge.org) contributor Jason Yuen on June 25th 2024.Antihydra is a sequence starting at 8, and iterating the function 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.
BMO#2 formulation variant
Alternative statement of beaver_math_olympiad_problem_2_antihydra using set size comparison instead of a recurrent sequence b.
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).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) ↔`.Every convex set in has dimension at most 1.
For every there exists some such that every convex set in has dimension at most .
If , every convex set in has dimension at most 1.