(I'm the author of the game) Unfortunately it did not. That comment was made when I was optimistic that an undergraduate who'd added more levels as a summer project would go on to PR them, but then the term started and they were distracted by their degree. We have some kind of prototypes for even/odd world (e.g. "prove odd * even is even") and prime number world (boss level: prove 2 is prime), plus a hard world consisting basically of unsolved problems such as Goldbach, Twin Prime Conjecture etc. But they never made the transition from "lean file containing a bunch of theorems" to "lots of files each containing one theorem and some rambling".
Sure--I think I saw a very old version of this, so most of it is new to me--but it also refers to "Prime Number World and more", and at least Prime Number World doesn't seem to be on the map.
(I'm the author of the game) Unfortunately it did not. That comment was made when I was optimistic that an undergraduate who'd added more levels as a summer project would go on to PR them, but then the term started and they were distracted by their degree. We have some kind of prototypes for even/odd world (e.g. "prove odd * even is even") and prime number world (boss level: prove 2 is prime), plus a hard world consisting basically of unsolved problems such as Goldbach, Twin Prime Conjecture etc. But they never made the transition from "lean file containing a bunch of theorems" to "lots of files each containing one theorem and some rambling".
thanks! (in particular, for updating the "ℕ is a total order" for Lean 4)
"Algorithm World" was new to me
Sure--I think I saw a very old version of this, so most of it is new to me--but it also refers to "Prime Number World and more", and at least Prime Number World doesn't seem to be on the map.