I'm surprised some people think this is a matter of checking whether formal sentences match some English sentences lol
It is a matter of checking whether formal sentences match mathematical statements, which are written in natural language.
Imagine someone saying "just write good English lol eventually you can do good math". I'm aware you're not quite saying this but you seem really distracted by the human language representation of math, connecting doing math proofs to generating English sentences from some probability distribution is ridiculous. Of course it is possible LLMs can do math, if it's matter of having nonzero chance, there's also a nonzero chance we are all brains in vats. More rationally if someone says something is possible they should produce some evidence that it is possible. And then we decide whether that evidence is good enough.
Writing well in any human language is not good enough, since it is entirely different from being able to tell whether a set of formal axioms capture certain ideas about a mathematical structure. This is a model theoretic issue. Neural network theorem provers deal with proof theoretic issue.
The best LLM-Lean provers right now are tackling the very challenging problem of how to generate the right sequence of tactics for infinite search space, all relying on, excuse me, undergrad students to formalize proofs and statements for them.
>to see why you would assume an invariant speed, the assumption isn't just pulled out of thin air at the start
It's not out of thin air, it's from a very empirically successful theory: Maxwell's electrodynamics. The problem back then was that this theory was not relativistic, i.e. the speed of electromagnetic wave in Maxwell's equations was the same under all reference frames. So you either abandon the idea that laws of physics remaining the same under all reference frames, OR abandon Galilean velocity addition.
Einstein's approach was modifying the latter so that it fits with the former, by imposing invariant speed. This was written in Einstein's original paper. It's not a mystery assumption.
It's also a very common procedure: two empirically successful theories have conflict and you need to resolve them by building something larger than both and reducing to both under limit.
I also agree we have gained insight into how kinematic structure is derived from algebra + physical constraint. Though you still need the physical insight to choose which physical constraint.
> It's not out of thin air, it's from a very empirically successful theory: Maxwell's electrodynamics.
That was the source of the assumption, yes--as you point out, Einstein said so in his original paper. But from the standpoint of mechanics, as opposed to electrodynamics, it was pulled out of thin air. There was no reason based on mechanics to make any such assumption. In fact, everyone else except Einstein that was working on the problem was looking at ways to modify electrodynamics, not mechanics--in other words, to come up with a theory of electrodynamics that was Galilean invariant, rather than to come up with a theory of mechanics that was Lorentz invariant.
> you either abandon the idea that laws of physics remaining the same under all reference frames, OR abandon Galilean velocity addition
Or, as above, you look for a Galilean invariant theory of electrodynamics. Of course we know today that that is a dead end, but that wasn't known then.
>if A sees B at speed v, then B sees A at the same speed v
is directly derivable from the Lorentz velocity addition formula which is the result of the usual two postulates. Why would you want that as an extra assumption...
Of course, if you already assume special relativity then this is baked in: taking the inverse of the Lorentz transformation matrix effectively sends v to -v. And velocity addition for sure already assumes you have the Lorentz transformations.
The point is that in the derivation of relativity from elementary postulates, the “reflectivity of velocities” assumption is used. For instance the linked paper uses it between equations (12) and (13). All such derivations use it at some stage.
Intuitively, “reflectivity of velocities” is why time dilation leads to length contraction with same gamma factor.
I don’t think it follows from absence of a preferred frame since one could imagine some complicated group structure relating the velocities of the various observers relative to each other in such a way that all are on equal footing and yet v_AB is not exactly -v_BA.
As mentioned, this is certainly a reasonable assumption but who knows what whacky alternatives are out there? After all, in the different context of quantum mechanics, such “obvious” relationships as xp = px no longer hold true.
Within historical context: This was said after Minkowski introduced the geometry for special relativity, which can be visualized on the `spacetime diagram`, now recognized as the vastly simpler and more efficient approach than the wall-of-text approach. Einstein initially had some difficulty, that was when he said this, but he caught up quickly.
>Strangely enough no personal contacts resulted between his teacher of mathematics, Hermann Minkowski, and Einstein. When, later on, Minkowski built up the special theory of relativity into his 'world-geometry', Einstein said on one occasion: 'Since the mathematicians have invaded the theory of relativity, I do not understand it myself any more'. But soon thereafter, at the time of the conception of the general theory of relativity, he readily acknowledged the indispensability of the four-dimensional scheme of Minkowski
Einstein, philosopher-scientist, Schilpp
And later Einstein expressed admiration for geometry again and again
>This problem remained insoluble to me until 1912, when I suddenly realized that Gauss's theory of surfaces holds the key for unlocking this mystery. I realized that Gauss's surface coordinates had a profound significance. However, I did not know at that time that Riemann had studied the foundations of geometry in an even more profound way.
Einstein, Kyoto Lecture, 1922
>I admire the elegance of your method of computation; it must be nice to ride through these fields upon the horse of true mathematics while the like of us have to make our way laboriously on foot
Hentschel (1998). The Collected Papers of Albert Einstein, Vol. 8 (English): The Berlin Years: Correspondence, 1914-1918
- You derived the theory correctly (end result should match textbook result) and thought what you were doing were wrong.
- No physicist you asked could explain where you were wrong
- No physicist you encountered could see the obvious connection of this and the usual approach
It's not really a mysterious or novel fact that you can have these shift of perspectives (at least since Kant who heavily influenced Einstein) e.g. Newton took his three laws as the base, derived relativity as a theorem. Einstein took (modified version) relativity (together with the invariant speed assumption which comes from electromagnetism) as the base and rebuilt the rest of theory of motion that reduces to Newton's theory in the limit. Nothing is amiss here.
Did you even read his post? what you are calling the "right" path is the "mathematician" path, assuming relativity + group structure.
What he complained about, the Physics textbook approach was the path taken by Einstein who started from the "invariant speed" assumption to derive relativity:
>"introduce another postulate... namely, that light is always propagated in empty space with a definite velocity c which is independent of the state of motion of the emitting body."
There's also nothing really "wrong" with Einstein's approach either, it's motivated by physical constraint from Maxwell's electromagnetism.
Mathematician's approach is motivated by imposing logical constraint of an abstract mathematical structure (group of transformations from one coordinate system to another)
The two turn out to be connected (physical constraint selects a math model from alternatives). Nothing really strange.
Imagine someone saying "just write good English lol eventually you can do good math". I'm aware you're not quite saying this but you seem really distracted by the human language representation of math, connecting doing math proofs to generating English sentences from some probability distribution is ridiculous. Of course it is possible LLMs can do math, if it's matter of having nonzero chance, there's also a nonzero chance we are all brains in vats. More rationally if someone says something is possible they should produce some evidence that it is possible. And then we decide whether that evidence is good enough.
Writing well in any human language is not good enough, since it is entirely different from being able to tell whether a set of formal axioms capture certain ideas about a mathematical structure. This is a model theoretic issue. Neural network theorem provers deal with proof theoretic issue.
The best LLM-Lean provers right now are tackling the very challenging problem of how to generate the right sequence of tactics for infinite search space, all relying on, excuse me, undergrad students to formalize proofs and statements for them.