[justinpombrio]

Bah, I almost talked about what would happen if you did this on a sphere. Yes, there is an assumption that rotations and translations are commutative and associative. We're so used to this that our intuitions sensibly hide it.

The fact that there are hidden assumptions doesn't invalidate the proof, though. There are always hidden assumptions. Even if I give you formal axioms to reason with, you need a system in which to interpret those axioms.

[whatshisface]

Although I see the reasoning, I'm still not comfortable with the proof. It sounds to me like "plug something in to the Zeta function, observe that it isn't a nontrivial zero, conclude that there are no nontrivial zeros." Even if it seems completely intuitve to me I still wouldn't consider it proven.

[justinpombrio]

Interesting. For me, there is no clear gap between intuitive proofs and formal proofs. Sure, intuition can lead you astray, but as you do mathematics, you develop your intuition so that you stop being intuitively certain of false things. Contrariwise, formal proofs are more likely to contain dumb algebraic errors, but as you do mathematics you learn to be exceedingly careful in your calculations.

But the wider point I want to make is that there's no gap between the two. _Real proofs aren't fully expanded._ If you've worked with a theorem prover like CoQ, it becomes painfully clear how many steps even the simplest proof skips. For example, the proof that the sqrt of 2 is irrational is really easy:

https://www.math.utah.edu/~pa/math/q1.html

But look at how many steps this skips, if you want to get close to actual axioms and definitions:

- You squared both sides of an equation. In this case, that's fine because you're only doing forward reasoning, but if you wanted to reason backwards you'd also have to check that both sides had the same sign to start.

- You multiplied by q^2. That's only valid if q^2 is nonzero. Now intuitively we know that q^2 is nonzero, since q is nonzero. But it needs a proof.

- You deduced that p was even from the fact that p^2 was even. How do you prove that? My first thought is to use the fundamental theorem of arithmetic. I don't know about you, but my intuition completely glossed over the fact that the proof that sqrt(2) is irrational made use of the fundamental theorem of arithmetic when I first read it. Either that, or there's another way to prove this; what is it?

Now, you could expand this proof to include all the steps. But we don't bother, because it's painstaking and not actually that likely to catch flaws in the proof, because we intuitively know these things. Likewise, I feel like the triangle proof is the same way: it skips over some things, but we intuitively know it's okay and you could expand it (to talk about commutativity of translation and rotation) but there's usually not much reason to bother.

Although it's a lot more obvious how to go about expanding the proof that sqrt(2) is irrational, I'll give you that.

[whatshisface]

There is an implicit, widely-held sense that the detail in proofs should scale with the expected training of the people who will be reading them. If your intended audience has internalized their field so well that the expansion and checking happens completely automatically and subconsciously, more power to them - but on the other end of the scale you have the proof that the square root of two is irrational, or this one about interior angles. Other than machine-aided proofs the most thoroughly expanded you ever see anything is in highschool geometry!

So, what justifies this scheme? I would say that once you have seen a technique used in full detail, you don't need to see the detail elsewhere because there's a meta-theorem in your head that applies to every case where things line up in a pattern where the technique works. Slowly this replaces your natural intuition.