Will crowdsourced proofs be more acceptable than computer proofs? Should they be? Would it still be possible for one person to survey the proof?
Also, you've got a link you need to fix.
1: Probably; computer proofs should be more acceptable but there's nothing wrong with crowdsourced proofs; hrmm, maybe.
All in all, this is really neat. It's cool that someone working alone was able to get the problem in a form that the crowd could improve upon. I wonder what sort of problems lend themselves to that? Problems that are about tightening up bounds (like this), or problems that can be split into a large number of cases (like the four-color theorem) seem fertile ground.
This is all a metaphor, right? For every lonely person feeling all alone way out in the middle of nowhere there's just got to be another lonely person right nearby feeling just as alone.
Computer proofs are, like, accepted with some regularity, no?
Crowdsourcing in this case does not seem terribly different from traditional academic discourse, given that most of the people weighing in appear to be working mathematicians. It's more like several dozen mathematicians publishing many tiny papers than asking people on amazon to draw a sheep or whatever.
This is the "assume a spherical cow" usage of "slightly generalised", right? Or is there good reason to think that there's no principled distinction between actually sequential and separated by some small but non-zero number of non-primes?
Why doesn't somebody try to breed a spherical cow? They could maybe cooperate with the guys trying to breed a perfect red bull so the world will end.
6: I thought one of the major computer proofs was refused peer review on a combination of philosophical and practical reasons? I don't recall which one--maybe the original four color theorem, or one of Thomas Hales's proofs?
Admittedly, peer review of a computer proof should be easier, as it should just consist of checking that the assumptions and conclusion are what the writer says they are, and then running the provided Coq file.
Back on topic, yes, this does sound like regular math discourse (assuming they structure the Wiki or whatever into a way that each small unit can be conveniently verified). If anybody has philosophical objections because there's so much content that no single human could read it all, they're on weak ground.
in very short order (a month), the separation went from 60 million to ~6,000. The participants seem to have squeezed most of the juice in this low-hanging fruit, though: the subsequent six or so weeks have gained them just another factor of 10.
You're reading the wrong column in the Polymath table. The column you want is H, which is currently down to 4,680 (subject to checking, of course).
perfect red bull
A novel technique! Most researchers trying to improve the vodka red bull are focusing on the vodka part.
the original four color theorem
It was definitely resisted at first but that was thirty years ago or whatever. And it has now been accepted, looks like.
Computer proofs are, like, accepted with some regularity, no?
Aren't the homotopy type theory guys going on and on about how their proofs are all computer-checkable in Coq or Agda or whatever?
Anyway, I am sympathetic to the "too pretty not to be true" line.
Computer proofs seem pretty unsatisfying to me. I guess I tend to think the goal of mathematics is generating understanding, not generating theorems. But, of course, there are plenty of giant proofs that can't be fully grokked even if they are human-generated, so maybe that's not a very consistent thing to think.
Red heifer, I think, not red bull.
http://www.unfogged.com/archives/comments_11661.html#1366808
Anyway, I am sympathetic to the "too pretty not to be true" line.
How often do people try to pick you up with it?
How often do people try to pick you up with it?
Hey bay-bee are you a morphism from [too early to think of what would go here]? 'Cause you're lifting my cock right now.
Computer proofs seem pretty unsatisfying to me. I guess I tend to think the goal of mathematics is generating understanding, not generating theorems
I guess I don't understand why computer proofs don't generate understanding? Well, I can see why they wouldn't when you have the computer exhaustively check 35,000 edge cases or whatever. I suppose I was thinking of computer-assisted proofs.
13: Yeah, the constructiveness of it is (as I imperfectly understand it) one of the big draws.
I guess I don't understand why computer proofs don't generate understanding?
I don't think they're unsatisfying, but I can see a couple ways that they can fail to generate understanding:
Are computer proofs usually presented as just pure theorems in whatever formal system they're occurring, or are there systems to automatically chunk them into quasi-human-readable portions? The former can fail to generate understanding because it's a lot like reading assembly code--it's too low level to understand what's going on.
Alternatively, sometimes the computer can find some weird path that's completely unintuitive, like the way machine learning algorithms sometimes do. Optimizing for some property might get you to the desired (and perhaps even 'best') solution but not necessarily in a way that makes it intelligible.
And, yeah, the 35,000 edge case thing is an issue. Mathematicians tend not to like disjunctions that have more than, like, three cases.
7: The big breakthrough was any bound at all. The step from infinity to 60 million is a lot bigger than the step from 60 million to 2. Zhang's proof is insanely technical, while I think the subsequent improvements are either more-careful versions of Zhang's proof, or involve combining Zhang's techniques with other standard techniques in number theory.
12: There are now three different computer proofs, one of which actually generates a proof that can be checked by a standard proof checker.
19: Computer proofs don't generate understanding if they are long, which the most famous ones are. There are a couple of results that have been found by computer that have been short enough that people have been able to rewrite them into humanly understandable proofs.
5: Nobody even paid enough attention to tell me how I got it wrong? This theory isn't saying that there aren't any totally lonely prime numbers, it just says that are some pairs of them everywhere, right?
humanly understandable proofs
How many humans have to understand something, so that we can say that it is "humanly understandable"? I think it has to be more than one. But can it be less than five?
22: Right. The twin prime conjecture is that there's infinitely many pairs of "twin primes" (numbers n-1 and n+1 such that both are prime), not that all primes are in such pairings. As a counter-example, 23 is prime but not a twin prime.
But the metaphor is lovely. Math is just a country song.
Not sure if it was intentional, but I am grateful that you kept links to my blog off the front page.
Computer proofs don't generate understanding if they are long, which the most famous ones are. There are a couple of results that have been found by computer that have been short enough that people have been able to rewrite them into humanly understandable proofs.
That's the difference between computer proofs and computer-assisted proofs that Nosflow mentioned above, right. The objection, which I think is still colorable, is that a proof should be like an explanation. It should give an actual human being an actual understanding of why something is true. Computer-assisted proofs wind up being surveyable, so they aren't objectionable.
Also, a lot of computer proofs are (or used to be) not even complete surveys of all the cases. They used a combination of statistical methods and random checking of cases to get the conclusion that the odds of the theorem being false are vanishingly small. This also doesn't seem to work as an explanation of why something is true.
22: yeah. So, if you're feeling totally alone, then it might be because you just haven't met the other half of your pair - in which case have faith! he or she must be less than 60 million places away from you! - or it might be because you really are just alone.
One and one seems so simple
But we always somehow get it wrong
Turns out that math
Is just a country song.
The big breakthrough was any bound at all. The step from infinity to 60 million is a lot bigger than the step from 60 million to 2.
Oh sure, I can see that. I was just curious as to whether it's in the nature of the post-infinity narrowing that (people feel) eventually they'll get to 2, or if it will require entirely new techniques/approaches.
27: Yes, it's like the thing in Waiting for Godot with the two thieves.
10: Gareth, indeed, I made a mix-and-match error--meant to say that they went from 60M to 60k, and then down another factor of 10. Thanks for pointing out the error.
15: You definitely did, but I just wanted more threads.
25: Not intentional, no, but glad to help.
Do I have it right that you there should be lots of lonely primes, since asymptotically the gap between primes of order N grows as log(N)? For large enough N prime numbers could become arbitrarily lonely, right?
15: You definitely did, but I just wanted more threads.
I like the math threads. It's fun to realize that there's another group of expertise on unfogged which hasn't gotten as much screen time as the lawyers or programmers.
32: Yes. In fact you can be constructive about it: n!+2, n!+3, n!+4 ... gives an arbitrarily long string of composites.
32: arbitrarily lonely? Christ, essear, this is bringing me close to tears. I will seek reassurance from Tim Minchin:
Your love is one in a million
You couldn't buy it at any price
But of the 9.999 hundred thousand other loves
Statistically, some of them would be equally nice
Or maybe not as nice but, say, smarter than you
Or dumber but better at sport or tracing
I'm just saying
I really think that I would
Probably have somebody else
If I didn't have you
Someone else would do
I'm going to put in my usual pro computer proof argument. It's overstated how "beautiful" most arguments are. Most theorems (especially ones that weren't found centuries ago) have beautiful ideas but also involve a part where you just have to work out some stuff. Often this means taking a few cases, or doing a calculation that you're not sure is going to work out. I don't see why that's so different from a proof where you have a few beautiful ideas and then have to do ten thousand cases to see that those ideas are enough to finish the argument. I'd certainly rather have a computer proof where the argument is reduced to a few understandable ideas that are simple enough that a computer can just go use them, than a human proof that stretches over dozens of articles each containing new hard ideas that can't be automated.
If you really understand an idea than you should be able to teach a computer to use it. So computer proofs often show deeper understanding than human proofs.
34: It's not clear to me how the existence of arbitrarily long strings of composites proves anything about arbitrarily lonely primes-- couldn't primes lie in pairs on one side or the other of that string of composites?
36 is interesting. I'm probably importing my bias at the way people use computers in my field into a context where it doesn't make as much sense.
37: That same objection applies to your 32.
39: Oh yeah good point. So is there a simple argument for the existence of arbitrarily lonely primes?
35: Well, I thought the way to spin it for peep would be "don't worry, no matter how lonely you are there are always people prime numbers who are much, much lonelier," but maybe that isn't so comforting after all.
The carbon-based chauvinism in this thread is appalling.
If by "lonely" you mean gaps on both sides, that's much harder. It certainly doesn't follow from the PNT (as in your first comment) since the gaps could alternate large/small. It's probably still known (or known subject to Riemann), but I couldn't find it anywhere explicitly. Everything about gaps seems to be looking at the gap between consecutive primes, not the gaps on both sides of a single prime.
So is this some kind of a Moebius thread where essear has gone back in time and changed Twin Primes to Lone Prime by running some poor number over in his metaphorical Delorean?
If by "lonely" you mean gaps on both sides, that's much harder.
Maybe in a decade it'll be a new Millennium Problem, known affectionately as "The Peep Conjecture".
It's known that twin primes are "sparse" in the sense that the sum of their inverses converges. I would guess that similar arguments would tell you that primes with another prime within distance n are also sparse in the same sense. This would tell you there were arbitrarily lonely primes.
In a thousand years, civilization will be rebuilt based on the vellum printouts of TFA.
It's known that twin primes are "sparse" in the sense that the sum of their inverses converges.
That is a lovely formal definition for sparseness. I need to be able to explain that concept for fluently.
"more fluently". Not much fluency about.
It's a good notion of "sparse" because it behaves well under unions. The union of two sparse sets is still sparse. That's nice because if you know that pairs p, p+2 are sparse, you also know that primes where either p+2 or p-2 is prime is sparse because it's the union of two sparse sets. This means just from knowing that pairs p,p+k are sparse for all k you automatically get that primes with another prime within m are also sparse, and hence a "dense" subset of the primes are m-lonely. (Here "dense" means the compliment is sparse, and in particular dense sets are automatically infinite.)
Since the primes themselves are dense, does this mean that the non-twin primes must also be dense.
Yes, non-twin primes are dense. (I.e. the sum of the inverses of the non-twin primes diverges roughly as fast as the sum of the inverses of all primes (namely like log log N).)
50: how do you know the sum over k converges?
Oh, wait, k is less than m by definition in your formulation. Right.
Yeah. If you want to look at primes with another prime within 4 that's the union of primes with one 2 over, 4 over, 2 under, and 4 under. So the sum is bounded by the sum of those four, and so is finite (assuming that the theorem about sparseness of twin primes generalizes, but surely it does).
I was sure this post was going to end with H-G providing the proof.
58
There aren't even any margins to put it in.
One of the favorite things I ever read by Donald Knuth is somewhat relevant to the OP. It was one of his several "Theory and Practice" talks/papers (I believe it is the one collected in Chapter 7 of Selected Papers on Computer Science; I saw it as reprint of a talk he gave in Athens). Not available to me to check, but in the version I read, IIRC he contrasted developing TeX with his prior experience working in theoretical math. He suggested that the original detailed specification for TeX amounted to a several-hundred page proof that TeX would behave correctly. If it had been a theoretical math paper he suggests that with both peer review and publishing a small number of people would have read it and few errors would have been found and corrected. As it was, there was the grueling effort of getting it to actually work. Which, of course, was fabulously successful and led to the famous exponentially-growing bug payment scheme*. (My recap sucks, those with access go read it.)
*Per this great interview (everyone go read it):
In software I similarly pay for errors in the TEX and METAFONT programs. The reward was doubling every year: It started out at $2.56, then it went to $5.12, and so on, until it reached $327.68, at which time I stopped doubling. There has been no error reported in TEX since 1994 or 1995, although there is a rumor that somebody has recently found one. I'm going to have tolook at it again in a year or two.
Does anyone here have (or know someone who has) a Knuth reward check? (A lot more common for errors in his books than his software.)
61: I'm kind of fascinated by this idea that writing a mathematical proof should be more like writing computer code. I think it's interesting that writing code is usually an interactive process (since you can easily *run* the code and see what it does), whereas writing proofs is much less interactive (it's not as easy to write down a proof and figure out whether it's correct). That kind of interaction seems really useful for some problems, where you can make progress incrementally, by trial-and-error; but it may be less useful for problems where you need to find the right idea first, and then figure out how to state it precisely.
In my limited experience, you can make progress in code-writing without understanding. I frequently find myself saying things like "hmm, maybe it will work if I move this line before this line" and bingo, it does. But I have no idea why.
This might be something that is more common for novice programmers, but it is still definitely something that can happen, which shows some divergence between proving things and programming.
I can remember when we had to write the code and then walk across campus and rouse a work-study student to get the printout to see if it worked.
I was going to mention the onions on our bets, but it occured to me that reference is itself twenty years old.
We wore onions on our references, as that was the style of the time.
A slight tweak to apalike.sty makes it easy.
which shows some divergence between proving things and programming.
You think no one using Language, Proof, and Logic has ever tried moving the order of statements around to get a valid proof?
I calculated a tip while drunk, so probably.
62, 65: a friend of mine got one in the past couple of years.
15 Sorting Algorithms in 6 Minutes.
The link in 76 is better with the sound off.
To the OP, Dor/on Zeilb/erger is a combinatorialist who relies heavily on computers and often takes the extreme position that math proved using computers is deeper than "mere human" math. He expresses this view in a manner that looks identical to crackpottery (e.g., here). And credits his computer as co-author. In other words, eccentric mathematicians are often eccentric. Reading his opinions page is fun, though.
I dunno, bogosort sounds kind of nice.
67: 15 years old, only, he said, pedantically.
80: Huh, I guess it is 20 years old. Stupid internet.
78: he does seem a bit of a crazypants.
77: Yeah, it really is the visualization which is interesting.
78 reads to me as idiosyncratic but not at all crackpotterish. But I've been spending too much time lately thinking about anthropic arguments and other marginal things, so maybe I'm a crackpot too.
84: Agree. In general, I think the role of networks (of people and computers) in our understanding is not given its due. Continuing to advance in depth across the broad swath of knowledge increasingly demands it.
It's going to be quite a treat watching essear transform from jet-setting physicist to another Archimedes Plutonium over the next several years.
86: Did not know he'd moved on from Ludwig Plutonium.
I moved out of Lu/bo/s Mot/l's old office to avoid becoming a right-wing crackpot.
I don't know that Archie is right-wing, particularly.
A crackpot physicist without a death ray is pathetic. A crackpot physicist with a death ray is a ruler of men. Keep that in mind, big Ess.
Fiddlesticks! Crackpot physicist death rays don't even slow them up.
78: Reading his opinions page is fun, though.
Yes, am enjoying them. From #32 I learned of the lack of scruples of theoretical scientists:
The Black-Scholes formula started a whole new cottage industry of `rocket scientists', who were hired by Wall Street to implement the formula. HOWEVER, Very Few Mathematicians were hired! They were considered too slow, cautions and pedantic. Instead, hundreds of theoretical physicists, who do not have any scruples using approximations without rigorous error bounds, were preferred.
Also, one of his opinions led me to read up on Robert Trivers (evolutionary biologist whose work is the basis for much of Dawkins' stance in Selfish Gene). He was in history intending to be a lawyer, but had a breakdown because [he] stayed up "all night, night after night" reading Ludwig Wittgenstein. Via a circuitous route he ended up in Biology at Harvard (but was denied tenure). He also co-authored a paper with Huey Newton, " Trivers, R.L. & Newton, H.P. Science Digest 'The crash of flight 90: doomed by self-deception?' November 1982, pp 66,67,111."
92: Them's fightin' words!
93: he ended up in Biology at Harvard (but was denied tenure)
Not that that can be taken to imply anything, really.
70: Yeah, but if they relied on that technique all the time, I would say they didn't understand how the proof worked, which meant that for them at least, it wasn't working as a proof, which is meant to bring understanding.
I'm going to talk myself out of believing computer proofs.
94.last: Yeah, I don't know what happened, but wonder if there was some manner of back story. His stuff was also the theoretical basis for some of the controversial part of E. O. Wilson's Sociobiology which was at the center of a massive and nasty fight at Harvard at the time. (He also seems to not be someone an administration would be likely to like, someone about to become best friends with Huey Newton when he went to UC Santa Cruz. Also occasional later flare-ups of his mental illness, and an incident where a Rutgers colleague called the police on him.)
Is this the sex thread now? 'Cause I feel like this story should come as no surprise to astute readers of The Monkey-Wrench Gang, but even so, damn, some people take this family drama thing to truly Achaean levels!
I wonder if a certain rider up San Juan Hill has any thoughts on it?
94.last: Yeah, I don't know what happened, but wonder if there was some manner of back story.
As far as I understand, H/rv/rd didn't even have a tenure track until sometime less than a decade or so ago. Every tenure case was treated as an open search. The tenure rate was... not high. So I'm not sure there has to be a story. (Tenure is still dicey, but at least now the cases are treated as coming up for a promotion instead of an open search.)
Tenure track? They didn't even have vowels!