Q-Q

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.

What are you guys on about

>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...

https://en.wikipedia.org/wiki/Velocity-addition_formula#Spec...

vAA = (vAB + vBA)/(1+(vAB*vBA/c^2) -> 0 = vAB + vBA

so velocity of A relative to B and B relative to A both have magnitude v.

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

I find it not believable that

- 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:

https://sites.pitt.edu/~jdnorton/teaching/HPS_0410/chapters/...

>"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.