54 karma · joined July 19, 2023
In the sources I see that the acceleration is applied simply by utilizing a velocity‐addition formula (see https://github.com/dbrant/relativity/blob/fcc20fb18381959ac2...), so no Wigner rotation appears. I guess all the fancy stuff related to how time passes in an accelerating frame (like https://en.wikipedia.org/wiki/Twin_paradox#Difference_in_ela...) is also wrong in this simulation because of that.
You can however observe a mathematically equivalent effect in hyperbolic games, e.g., in Hyperbolica. Hyperbolica even has a quest about rotating a chest by moving it along the axes. On the hyperbolic plane it’s of course not about acceleration but about a winding number you’re doing around some point, but it’s still fun.
Also the original Metro design as in WP 7/8/8.1 or Windows 8/8.1 relied heavily on the pure text, and the only place populated with a lot of icons was that iconic tiled start screen, although this is probably not what you mean.
But in this case, as using plain brute force is already quite a common thing in searching for counterexamples, using LLMs as a sort of more advanced brute force seems to be just the right thing to do, so I struggle to understand so much hostility to this approach.
The reason is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.
>Requiring explicit proofs for every subtraction was presumably seen as too onerous.
Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.
>Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".
What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.
You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?
There were some proposals like compressing all the .olean files, but (as far as I know) none of them were implemented. Well, even if some proposals were implemented, their contribution was effectively negated anyway.
On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:
def x := #[1, 2, 3, 4]
#check x[7]
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
Sadly, this clone looks very‐very bad, just like millions of WP8‐like launchers compared to the actual WP8.
>But the infinitesimal methods used before epsilon-delta have been redeemed by the work on nonstandard analysis.
This doesn’t mean that these infinitesimal methods were used in a rigorous way.