An impressively terse presentation, but that makes it not particularly clear or likely to spark further understanding in someone who doesn't already understand the phenomenon intuitively.
Here's the approach I prefer for clarity and understanding:
First, recognize that prime p can be written as a sum of two squares just in case A^2 + B^2 = 0 (mod p) has a nonzero solution. In one direction (left to right), this is obvious; in the other direction (right to left), given A^2 + B^2 = kp with A and B indivisible by p, we can compute A' + B'i = gcd(A + Bi, p) in the Gaussian integers using the Euclidean algorithm. The result is a proper factor of p; however, it is not 1, as A + Bi is not co-prime to p (if it were, so would be its conjugate, and therefore so would be their product A^2 + B^2 = kp, which clearly isn't). Thus, |A' + B'i|^2 = A'^2 + B'^2 is a nontrivial proper factor of |p|^2 = p^2, which means A'^2 + B'^2 = p on the nose.
Next, recognize that A^2 + B^2 = 0 (mod p) just in case (A/B)^2 = -1 (mod p). [Recall that we can do division in arithmetic modulo a prime; in jargon, such arithmetic comprises a "field"].
Thus, the question of which primes can be written as a sum of two squares reduces to the question of which primes admit a square root of -1 in their modular arithmetic.
Finally, we can apply Euler's criterion to this, which tells us x is a square modulo odd prime p just in case x^((p + 1)/2) = x (mod p) [I can expound on why this is true in more detail if readers are interested; essentially, there are (p + 1)/2 many squares modulo p (one is 0, and other (p - 1)/2 come from the other values mod p paired off under negation), and Fermat's Little Theorem tells us they're all solutions to this equation]. Applying this criterion with x = -1, we see that -1 has a square root modulo odd prime p just in case p is 1 (mod 4), which, by all the above, means an odd prime is a sum of two squares just in case it is 1 (mod 4).
Pushing further on the ideas above by thinking about factorization of Gaussian integers more generally gives us more: it gives us a convenient formula for exactly how many ways there are to write an arbitrary integer N as a sum of two squares. (And by carrying out the analogue with quaternions rather than complex numbers, we get a formula for four square representations as well). But, again, all this I will leave to followup discussion if desired.
I'm a grad student in math and I can say that sentences like this are quite typical in published proofs. Details are often omitted (though I just found a mistake in a paper hidden in a 'left to the reader' statement).
Obligatory links to Lamport's "How to Write a Proof" [0], and "How to Write a 21st Century Proof."[1] A video presentation of the latter is discussed at [2].
I can't seem to find it, but I was under the impression that some famous mathematician (I had Erdos in mind, but that's clearly wrong) solved an open problem during a math olympiad in the 1950s. Perhaps that was just an tall tale our trainers would tell us, though!
Speaking of uncountability, here's a similar one for why the set of functions N->{0,1} is not countable. If f:(N->{0,1})->N were a bijection, let g(t)=1-f^(-1)(t)(t), and compute g(f(g)).
Anyway, whether something counts as a proof is a matter of whether you (logically) accept it as irrefutable evidence. As with any genre, you have to consider your audience. I hear gauge theorists are content to have as a proof a couple of references to a couple papers which have techniques which apply, with minor alteration, to the current problem.
That said, I wouldn't have minded if Zagier actually demonstrated it was an involution with exactly one fixed point!
I love this theorem. Proving it was, for a while, my equivalent to "counting sheep" when I couldn't sleep.
The approach I used was the one that works through the Gaussian integers, which relies mainly on the facts:
-- Both the Gaussian integers and the usual integers are Euclidean domains, and hence in particular are unique factorization domains.
-- Integer primes congruent to 1 or 2 (mod 4) are the norms of Gaussian primes.
-- Integer primes congruent to 3 (mod 4) just are Gaussian primes.
There are various ways to show that integer primes congruent to 1 (mod 4) are non-prime in the Gaussian integers. My currently favored approach is to show that x^2 + 1 is reducible in the ring of polynomials over Zp (the finite field of size p), which follows quickly from the fact that x^p - x factors completely over that field, which in turn follows immediately from Fermat's Little Theorem.
And Fermat's Little Theorem can be quickly proved by induction.
This is a nice proof. I just want to mention that it is also completely constructive - all objects involved are finite and so exhaustive search supplies the necessary instance of excluded middle.
We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones...
Every proof of this theorem, by any reasoning, would be constructive by the same criteria. You can always do an exhaustive search to determine whether p is a sum of two squares. (Of course, it's not obvious when solutions exist and when they don't; that's what the proof is for. But that doesn't come up in your evaluation of whether the proof is constructive.)
This is thus more a property of the theorem than a distinctive property of the proof. But, yes, the theorem is valid even in intuitionistic mathematics.
It's a bit more subtle than that. Operationally, the proof will end up being exhaustive search, but you also need a constructive termination proof.
This is not a very helpful way to think about these things though. What I meant is that all principles used in this proof are constructive. You could, for example, literally translate this proof into a proof in type theory.
Sure, but any classical proof of the theorem would automatically yield an intuitionistic (i.e., standard type-theory) proof as well; just run it through the double-negation translation, and then eliminate double-negations using the decidability of all relevant properties (i.e., of all instances of sub-formulae of the formula being proven).
In some sense, this is just what you were saying, but my point is, this phenomenon ends up arising inevitably from the nature of the proposition being proven itself, and isn't surprising or distinctive for any particular proof of it (even if phrased ostensibly classically, such a proof might well be regarded as implicitly constructive regardless).
For the vast majority of proofs you are exactly right. There are some exceptions, though, since you don't necessarily have a choice principle, even under a double negation translation. This is why you need Markov's priniciple in addition to the double negation transform to give a constructive intrepretation to proofs from classical analysis.
You could rewrite this proof using some results from point set topology which typically require choice (the article even gives an outline on how to do this, weirdly enough). This rewritten proof would be non-constructive in a more precise sense, in that you couldn't translate it step-by-step.
Sure, Markov's principle matters for some things, but it seems to me Markov's principle doesn't really matter for this particular claim ("for every prime p, such-and-such a decidable property phi(p) is true"), since the only unbounded quantifier is the initial universal one. Any classical proof of a Pi_1 (or even Pi_2, using the Friedman translation) proposition can be straightforwardly turned into an intuitionistic proof of the same proposition (technically, I mean specifically that Peano Arithmetic is Pi_2-conservative over Heyting Arithmetic [and I suppose there are similar results for stronger systems but we don't need those]).
So there is no surprise that this particular statement's proof is constructive, given that it is classically provable at all [again, technically, I am referring to classical provability in PA, but it would be shocking if Fermat's old proof, or any other anyone bothered with for a statement of this sort, had somehow relied on anything beyond PA]. For other more quantifier-complex classical theorems, it would be of more note to observe whether a particular proof could be made constructive (in the mere sense of intuitionistic mathematics) or not, but for this one, there's nothing to it.
Anyway, I think I'm arguing pedantically about something there's no reason for me to argue about at all. Sorry about that! I think we're both in agreement that this is great, its constructiveness is great, math is great. Hooray!
Yeah, I don't think we actually disagree here... all I was saying is that there are proofs which are genuinely non-constructive, and this isn't one.
You are arguing that this usage of "constructive" is basically meaningless for statements like this. It could only make a difference for artificial examples or artificially complicated proofs. This is definitely true.
To be honest, I shouldn't have brought this up in the first place. I know what the author meant by claiming the proof is non-constructive (it doesn't give a formula for computing x,y such that x^2 + y^2 = p), and this is the idiomatic usage of the word non-constructive for this particular field. It's just different from the rest of the world, but that's nothing new.
This is the terminology distinction fmap is noting with "We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones...". The PDF calls the proof non-constructive in that it does not provide an efficient algorithm; however, fmap calls it constructive in that it does provide an inefficient algorithm.
> We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones...
We do: the complexity classes P and NP. Ok, technically this is a polynomial time decidable language (does there exist etc. etc.), so perhaps consider FP and FNP (the function variants of P & NP).
Yes, this is a good idea. What I'm concerned about is that there is no standard terminology. The paper - and another comment in here! - is talking about the proof being "non-constructive", when in reality it is a constructive proof in 2-EXPTIME.
I'm only nitpicking here, because I'm seeing this a lot...
It's a shame that this site still has the annoying pop-overs asking for my email address, along with at least one bouncing and annoying "Click on me!" button.
Some context - knowing if a number can be written as a sum of squares can be reduced to determining whether its factors can be written as a sum of squares (proof of this involves the fact that norm of complex numbers respects multiplication). So the prime case becomes important. 4n+3 type primes cant be written as squares are either 0 or 1 modulo 4. 2 can be written. Which leaves the 4n+1 prime case which is fermats theorem.
I'm not a mathematician and it always amazes me how people can come up with this stuff.
How do you even start such a proof? (I know there are a lot worse ones). Does it just strike as a flash and you see the whole thing? or the general direction, and then you start tweaking it? I can't imagine what it's like.
