What's interesting about new proofs for existing theorems is that they can give new insights about the problem and create new questions to be solved. Sometimes they can link two previously unrelated ideas, and create entirely new fields of study.
Indeed, this is only natural. Mathematics may be unique in that a proof is often just as valuable an asset (and sometimes more so) than the "fact" that it proves. Another aspect of this is that in the best case an attempt to prove something or to find another proof could result in emergence of a new theory. (According to Grothendieck's viewpoint, this should be taken as a matter of principle - see http://www.landsburg.com/grothendieck/mclarty1.pdf.)
> Mathematics may be unique in that a proof is often just as valuable an asset (and sometimes more so) than the "fact" that it proves.
This is the HoTT point of view: a 'fact' is just a 0-truncated (or maybe I've got my indexing off) type, where all we know is whether it's inhabited (proveable) or uninhabited (unproveable). We get much more information from considering not just the bare fact itself, and not just even one particular proof of it, but the space of all possible proofs.
Also, is math really unique here? Maybe it is in the sense of having absolute proofs; but I'd imagine that, in disciplines where reproducible experiment is the substitute for absolute proof, it is also true that the experiment is often as valuable as what it establishes, and that, the more kinds of experiments (not just the more trials of the same experiment) there are to establish the same thing, the better.
Your indexing is off :) Propositions (or 'facts' as you call them) are the (-1)-types, whereas 0-types are usually referred to as sets. A way to remember this is that the path-spaces (i.e. equalities) in a set are propositions, bringing you one level down.
While you're right that "proof relevance" is one of the key features of HoTT, I don't agree that what's being described here "is the HoTT point of view". Any mathematical proof bears on techniques that may be interesting beyond the proven result itself; HoTT doesn't clarify or elucidate that, nor does it aim to.
> I don't agree that what's being described here "is the HoTT point of view".
I am no expert in HoTT, so I certainly defer to what sounds like your expertise here. I should probably have said something closer to the weaker statement "this reminds me of HoTT", which hopefully is not incorrect—although you're right that what I really had in mind was proof relevance.
The HoTT n-type stuff is orthogonal to this. Fermat's last theorem is a singleton in HoTT, so any two proofs of it are equal in the HoTT sense, but new proofs would still be considered valuable.
I am no expert in HoTT, so I should definitely defer to you here; but I thought much of the power of HoTT was the ability to analyse a whole space of proofs without collapsing them to a single proof, so I'm surprised to hear it. Is your statement an informal observation, or a proveable fact? Is it true about a wide class of propositions, or is there something special about FLT?
That statement is a provable fact. FLT is "for all positive integers a,b,c and n > 2, a^n + b^n != c^n". Equalities and disequalities on natural numbers have no interesting proofs in the HoTT sense. That is, when x,y are natural numbers, x=y is either the empty type or the unit type. Formally, if FLT is the statement of Fermat's last theorem, we have isContr(FLT), which means that FLT only contains a single point.
The issue is that the terminology that is used in HoTT is highly confusing and contradicts conventional terminology. The word "proof" is used when it would be clearer to use the word "point" or "evidence" or "witness". With conventional terminology, there clearly are multiple proofs of FLT. But, when translated into HoTT, they all correspond to the same point/evidence/witness. It's similar to how there is only a single number 3, but there are many ways to write 3, for example as 1+2. There are many ways to write down the single point in FLT, and these correspond to different ways to prove FLT, but in the HoTT sense they are all equal.
A theorem in HoTT can have multiple points. This commonly happens when it is some kind of existence statement. For instance, the theorem "there exists a number greater than 3" has infinitely many points, namely 4,5,6,etc. Or a theorem "structures A and B are isomorphic" usually has infinitely many points. That statement means "there exists an f : A -> B such that f is an isomorphism between A and B", so it has one point per isomorphism between A and B.
Fermat's last theorem is not of this type. It is simply true, and the point/evidence/witness contains no data.
I’d say that’s not so unique (although few other fields have proofs in the first place!) Proof techniques are tools, and proofs are evidence that the tools that are used, work. Similarly in, say, sciences where experimental physics is a whole field unto itself, and devising and running new experiments has intrinsic value besides the evidence they gather. At least for the experimentalists themselves, the theoreticians might not agree =)
> Mathematicians Will Never Stop Proving the Prime Number Theorem
Entropy in the universe is finite (as far as we know). At some point mathematicians will not be able to continue trying to prove the prime number theorem. qed.
For extra rigour (!), replace "as far as we know" with one of the classic weaselly proof introductions: "Clearly, ..." , "It can easily be shown that...", "It is left as an exercise to the reader to show..."
It can be easily shown that entropy in the universe is finite. Thus, at some point mathematicians will not be able to continue trying to prove the prime number theorem. qed.
> It can be easily shown that entropy in the universe is finite.
Finite Universe can get stuck in a "dead" state. Giving infinite time, it will definitely will do so. The only solution for this problem is to have infinite Universe. Infinite Universe will never stop.
True, but the second law of thermodynamics states that the total entropy of an isolated system can never decrease over time. So I think the discussion at this point will revolve around whether a spacially infinite universe can be seen as an isolated system.
My original point was merely to use humor to caution against the use of "never", which breeds statements that are never true.
> the second law of thermodynamics states that the total entropy of an isolated system can never decrease over time
If you use this definition, then...
> I think the discussion at this point will revolve around whether a spacially infinite universe can be seen as an isolated system.
...it can't. "Isolated system" in the above definition of the second law means, basically, "a system that you can enclose in a box and measure its properties from outside". You can't do that with a spatially infinite universe. Actually, you can't even do it with a spatially finite universe, because even such a universe has no boundary and no "outside". So if you want to apply the second law to the universe at all, you need to use some other definition that can be applied to the whole universe.
Then one might also caution against the use of "never" in stating the second law of thermodynamics. It is a statistical law: the probability that entropy decreases in an isolated system is not zero, it is just extremely small. If you wait for long enough, it is bound to happen.
Surely this is only so if there were an infinite number of proofs of the Prime Number Theorem (assuming of course that new mathematicians are created every generation for eternity.)
I first thought that the occurences of "Math processing error" were a mathematical joke, showing that some quantity can not be computed. But reading the sentences again I think there should have been an equation...
If you believe in "The Book", it follows that someday mathematicians someday will stop proving the prime number theorem, and the fact that people keep proving it indicates that the Book proof hasn't been found yet.
I don't believe in The Book myself, I think which of multiple proofs is most elegant is largely subjective. But I'm not really a mathematician, just a guy who is interested in math.
Should every proof in the book be based on simple theorems or it's ok to have a "best proof" on advanced proofs.
(That is, assuming that the book is built on the current understanding of mathematics and not some other very different set of axioms)
But I'm afraid if I start talking about it too much we'll end in a confusion of Russel's paradox analogues trying to prove there are infinite possible books for the infinite possible sets of axioms describing math.
The mathematician Paul Erdős often referred to "The Book" in which God keeps the most elegant proof of each mathematical theorem. He once said "You don't have to believe in God, but you should believe in The Book."
Isn't most math that is published in journals just new proofs of already known mathematics? I have a hobbyist's interest in advanced mathematics, so someone else may correct me, but my understanding is that truly new mathematics is pretty rare, and usually depends on all the little advances in understanding that these new proofs and reorganization of mathematical knowledge provide.
Most maths is creation and exploration of the properties of new objects, or new structures of objects, without knowing if anybody will find them useful or make progress on any of the "big questions".
Nope, that's completely wrong. A new proof of a known theorem has to pretty damn cool to be publishable. It is much easier to publish theorems that were not previously known and the result is that most research papers are about new theorems not new proofs of old theorems.
I wish it were actually a little easier to get a new proof of a known result published.
I get a feeling that this applies to a lot of sciences.
I feel like in the field of computational complexity theory, people seem to find new ways of proving that a problem is NP-complete even though it's already been proved before.
Isn't this just about general curiosity, people just want to understand and explore a certain problem from different perspectives?
Not even close. The prime number theorem itself gives Li(x) as an approximation to pi(x), where Li(x) = \int_2^x dt / (ln t). (If you don't read LaTeX, this says "integral from 2 to x of dt / ln t". Li(x) can be numerically evaluated with pretty good accuracy.
The numerical value is 37607950280. Compared with the true value of 37607912018, this gives a relative error of around 1.0 * 10^-6, or 5 correct digits.
For those working on a language that supports automatic differentiation: implement such an algorithm, and differentiate it to get a primality test. I think that would be a good test for your compiler.
There's proof that there's an infinite number of prime numbers.
EDIT: It's actually a pretty simple proof.
First, recall that any composite number can be made by multiplying primes. If a factor is not prime, then it can be broken down further until you end up with only primes. For example, 60 = 12 * 5, but 12 is not prime and can be broken down further into 3 * 4, but 4 is 2 * 2. So the prime factorization of 60 is 2 * 2 * 3 * 5.
Second, assume that there is a finite number of prime numbers, and label them p1, p2, p3, etc, all the way up to pn, where pn is the highest prime number.
Multiply all the prime numbers together and add 1. Since this number has the form p1 * p2 * p3 * ... * pn + 1, if you try to divide it by any prime number, you will still have a remainder of 1. Therefore, this number will be prime.
Therefore, because you can always create a new prime by multiplying all primes and adding 1, there are an infinite number of prime numbers.
Why is it that posts from quantamagazine consistently appear on the front page, just to be debunked (though this one literally does not contain any substance!). Why do you upvote this?
Interesting fact about the Prime Number Theorum. It is NOT an estimate of the number of primes below a certain N but instead it is an upper bound on the number of primes. The classic formula derived from it, n/log(n), is always above the actual number of primes (except for very small 'n' (<10) where the approximation has significant error).
You can compare the actual counts of primes below 10^x (sequence A00688) to the estimates provided by the prime number theorum to see this (sequence A057835) for yourself.
Explanation:
At the risk of once again proving the Prime Number Theorum we can use a sieve to illustrate the upper bound. Above 2 there's an upper bound of 1/2 numbers possible being prime, since only 1/2 numbers are not a factor of 2. Above 6 there's an upper bound of 1/3 numbers being prime (only 1/3 numbers above 6 are not a factor of 2 or 3) and the cycle of multiples of 2&3 repeats every multiple of 6 so only 2 number remain that aren't a factor of 2 or 3 every multiple of 6. We could say above 30 (which is 2 * 3 * 5) only 8/30 numbers are possibly prime since only 8/30 numbers are not a factor of 2,3 or 5 on a repeating cycle. We could again create a sieve at 2 * 3 * 5 * 7 (210) with a repeating cycle of those factors (with 48/210 numbers remaining that aren't factors).
The prime number theorum can be derived from this upper bound.
So the prime number theorum is essentially defining the counts resulting from a sieve of primes. A sieve is an upper bound on the number of primes. Eg. there's numbers of the form 6n+1 or 6n+5 that aren't prime (eg. 25) that won't be filtered by that sieve but also aren't prime and as we've seen the prime number theorum can be dericed from this sieve. This is why the prime number theorum is an upper bound that always overestimates the actual number of primes below a certain number.
I suspect there are possibly ways to refine the prime number theorum further so that it's not always over estimating but i don't know how to do this. I can just understand why it's always an overestimate.
I'm afraid there are quite a lot of errors here. (Not everything in the following is pointing out errors, but most of it is.)
1. Yes, the quantity in the PNT is an estimate of the number of primes below a certain N. As usually stated among mathematicians, PNT is the statement that the number of primes up to x is asymptotic to Li(x), the logarithmic integral, and this is known to be sometimes over and sometimes under.
2. If you use x / log x instead of Li(x), then indeed it is known that once x isn't very small this is always an overestimate. But, again, PNT isn't the statement that it's an overestimate, it's the statement that it's a pretty good estimate. If Chebyshev or someone of the sort had proved that x / log x is an overestimate for the number of primes up to x, it would have been hailed as a fine achievement but not as a proof of PNT.
3. But your argument about "sieving out factors of a prime each time one is discovered" is not anywhere near to being a proof of PNT, let alone the stronger theorem that x / log x is an overestimate (which requires some concrete bounds on the error term in the approximation pi(x) ~ Li(x); the way you prove that x / log x is an overestimate is to show that x / log x is bigger than Li(x) by a certain amount, and then show that the difference between pi(x) and Li(x) is smaller than that certain amount; the latter is a strengthened version of the Prime Number Theorem).
4. The Wikipedia link you give is not saying that the Euler totient function is "a good way to derive the prime number theorem". It is stating a nice generalization of the prime number theorem that has the Euler totient function in its statement.
5. When you say "the prime number theorem is essentially defining the counts resulting from a sieve of primes. A sieve is an upper bound on the number of primes. [...] This is why the prime number theorem is an upper bound", I'm afraid this is completely wrong. If there is a proof of the prime number theorem that amounts to saying "look at this sieve, which easily gives an upper bound that's easily seen to be x / log x", then I don't believe anyone's found it yet.
> The classic formula derived from it, n/log(n), is always above the actual number of primes
No? pi(100) = 25, but 100 / log(100) = 21.7
The logarithmic integral is larger than pi for "small" arguments. But there is a pretty famous proof that li(x) - pi(x) changes signs infinitely often.