Skip to content

fix(Other): renamed BeaverMathOlympiad to BusyBeaverMathOlympiad #2386

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Paul-Lez merged 5 commits into from
Feb 27, 2026
Merged

fix(Other): renamed BeaverMathOlympiad to BusyBeaverMathOlympiad #2386

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e6df856
renamed BeaverMathOlympiad
Feb 23, 2026
7820f5f
renamed and fixed small inconsistencies
Feb 26, 2026
9e65971
Merge branch 'main' into renameBusyBeaver
franzhusch Feb 26, 2026
b0c5fc3
fix namespace error
Feb 26, 2026
800b2f6
Merge branch 'main' into renameBusyBeaver
franzhusch Feb 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions FormalConjectures/Other/BeaverMathOlympiad.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ Turing machine non-termination has been formally proved in Rocq, we indicate it
- [Antihydra wiki page](https://wiki.bbchallenge.org/wiki/Antihydra)
-/

namespace BusyBeaverMathOlympiad
namespace BeaverMathOlympiad

/--
[BMO#1](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#1._1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE_(bbch))
Expand All @@ -65,7 +65,7 @@ The machine was discovered by [bbchallenge.org](bbchallenge.org) contributor Jas
June 25th 2024.
-/
@[category research open, AMS 5 11 68]
theorem busy_beaver_math_olympiad_problem_1 :
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)
Expand Down Expand Up @@ -207,4 +207,4 @@ theorem beaver_math_olympiad_problem_5 : answer(sorry) ↔
∃ i, b i = f (a i) - 1 := by
sorry

end BusyBeaverMathOlympiad
end BeaverMathOlympiad
Loading