Thanks for making the game! I played it, and was a little frustrated that not all of your questions had the correct answers. For example, I recall one of the questions as reading, "How many typical transport protocols are on the internet?" which is not quite the same as what was answered, "How many internet transport protocols are commonly used?" You see, any protocol is "typical" for its use cases, even if it is uncommon. It reminded me somewhat of taking the SAT, where the test writers would replace a word with a more common word which doesn't actually quite mean what they intended. As the commenter below me pointed out, what he does with such questions is go meta--and I kind of like that perspective--but it was nevertheless a little frustrating. Overall though, I liked the game. Thanks for making it.
Note: I edited this the day after I wrote it because I found it a little too antagonistic, and I don't want to be antagonistic. I really did like the game, and appreciate that you made it.
You say that "Perhaps for several millennia, [rot didn't exist]" and then provide a date about 3300 years ago about when rot might potentially have began. You also say that several millennia is a "very, very long time". A millennium is 1,000 years. Do you think that life has only existed on Earth for a few thousand years?
Now, where did the weirdness come from here. Well, to me it seems clear that really it came from the fact that the reals can be built out of a bunch of shifted rational numbers, right?
I think the weirdness comes from trying to assign a real number measure, instead of allowing infinitesimals. I've never understood why infinite sets are readily accepted, but infinitesimal/infinite measures are not.
EDIT: To explain my reasoning more, suppose you were Pythagoras and your student came to you and drew a geometric diagram with lengths not in a ratio of whole numbers. You have two options here:
Finding the right extension is not an easy problem. Should we extend the numbers to allow square roots (including nesting), but nothing else? This suffices for geometry. But it's actually more useful to use something like a Cauchy sequence completion: Let any sequence of rational numbers that gets closer and closer together "converge" to a real number. Historically, extending your system of numbers has been what has worked.
When we come across an "immeasurable" set, this to me feels like the same kind of problem. Perhaps we don't yet have a general consensus on what the "right" extension is to infinitesimals/infinities. However, there clearly are some sets with infinitesimal measure, like the set you constructed. We should figure out a way to give that set infinitesimal measure, not just call it immeasurable.
To try to clarify why it felt self-referential. I think there's a self-reference regardless of whether you talk about classes or not, but it's more obvious if you talk about classes.
I think the correct mathematical term is "Impredicativity", not "self-referential", but I'm no logician.
If I were to try to translate this into classes instead of properties, it would look like, "The class of perfect properties contains the property of being every perfect property in this class". That seems self-referential to me.
An object is defined to be G if it has every perfect property, and then G is assumed (by axiom) to be a perfect property, hence being G requires being G. Now that I think about it a bit more, though, this seems more like a greatest-lower-bound situation than a Russell's paradox situation.
I didn't know that coherent logic was actually a term logicians used! I'm not a logician myself--I'm a programmer. Thanks for letting me know!
The reason I was saying it looked like a type error was because of the self reference. I'm extremely wary of self-referential definitions because you can quickly run into problems like Russell's paradox. It seems like sometimes it's okay to have self-referential definitions (like the greatest lower bound), but I'm not confident that Axiom 4 actually avoids those problems.
Could you please link me to that formalization?
Overall, the setup looks good, except for one part: I wouldn't give the remote machine complete access to your GitHub account.
I think maybe a better solution would be to set up a bare repository on the Nebius VM. This serves a second remote repository you can push to from your machine. After you push to the bare repository, you can clone it while only on the Nebius VM to another location on the VM. You can make changes in this second location, then push to the bare repository, which you can pull to your machine, and ultimately push to GitHub.
It is a bit more complicated than just directly pushing to GitHub, though. Maybe someone else knows a simpler solution.