Skip to content

Commit 448f15c

Browse files
authored
fix(Other): renamed BeaverMathOlympiad to BusyBeaverMathOlympiad (#2386)
Renamed BeaverMathOlympiad to BusyBeaverMathOlympiad to make it findable via search, when searching for BusyBeaver. Motivation was #2292
1 parent 5ccb2d2 commit 448f15c

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

FormalConjectures/Other/BeaverMathOlympiad.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ Turing machine non-termination has been formally proved in Rocq, we indicate it
3838
- [Antihydra wiki page](https://wiki.bbchallenge.org/wiki/Antihydra)
3939
-/
4040

41-
namespace BusyBeaverMathOlympiad
41+
namespace BeaverMathOlympiad
4242

4343
/--
4444
[BMO#1](https://wiki.bbchallenge.org/wiki/Beaver_Math_Olympiad#1._1RB1RE_1LC0RA_0RD1LB_---1RC_1LF1RE_0LB0LE_(bbch))
@@ -65,7 +65,7 @@ The machine was discovered by [bbchallenge.org](bbchallenge.org) contributor Jas
6565
June 25th 2024.
6666
-/
6767
@[category research open, AMS 5 11 68]
68-
theorem busy_beaver_math_olympiad_problem_1 :
68+
theorem beaver_math_olympiad_problem_1 :
6969
answer(sorry) ↔ ∀ᵉ (a : ℕ → ℕ) (b : ℕ → ℕ)
7070
(a_ini : a 0 = 1)
7171
(a_rec : ∀ n, a (n + 1) = if b n ≤ a n then a n - b n else 2 * a n + 1)
@@ -207,4 +207,4 @@ theorem beaver_math_olympiad_problem_5 : answer(sorry) ↔
207207
∃ i, b i = f (a i) - 1 := by
208208
sorry
209209

210-
end BusyBeaverMathOlympiad
210+
end BeaverMathOlympiad

0 commit comments

Comments
 (0)