Computer Assisted Proofs- still controversial?

Kenneth Appel, of Appel-Haken Four Color Theorem Fame, died recently. See here for an obit.

In 1972 I read that the four-color theorem was an open problem. From what I read it seemed like there was some progress on it (e.g., results like `if its false the graph has to be yah-big) but it seemed to be years away from being solved. I assumed that a new idea was needed to solve it.

Then, in 1976, it was SOLVED by Appel-Haken. From what I read it wasn't so much a new idea but very clever use of old ideas and a computer program. I also heard that it was just at the brink of what computers could do at the time, and that it would have taken 1200 grad student hours. (There is a good description of the proof on Wikipedia here.)

At the time I heard there were objections to the proof. Later when I read some of them they didn't seem like real objections. They boiled down to either

1. I wish there was a shorter proof. This is true, but not a reason to object.
   
2. It can't be hand checked. I trust a computer-checker MORE THAN a human checker
   
3. We don't know WHY its true. This is a more reasonable objection- but we do know how they got it down to a finite number of cases, so I'm happy with that.
   

In 1996 Robertson, Sanders, Seymour, Thomas was obtained a simpler proof. In 2005 Werner and Gontheir formalized the proof inside Coq- a proof assistant. To quote Wikipedia This removed the need to trust the various computer programs used to verify particular cases;it is only necessary to trust the Coq Kernel At this point I doubt anyone seriously doubts that the theorem has been proven.

There have been more computer-assisted proofs since then. See here for a list of some of them. That article also claims that such proofs are controversial and not always accepted. Is this really true? I thought the controversy was gone except for the topic of the next paragraph.

A famous computer assisted proof (or perhaps ``proof'') is the Kepler Conjecture. In 1998 Thomas Hale claims to have proven it. The proof involved rather complex computer calculations. The referees say they are 99% sure its true. Here's hoping an easier proof is found.

Computer assisted proofs may become more common. I just hope we still know WHY things are true.

Was Appel-Haken the first use of computer assisted proofs? I doubt it, but it was likely the first one to have an impact. It was important to know that this kind of proof could be done.

Is there a much shorter proof? A combinatorist once told me that since the function

f(n) = max size of proofs of statements of length n

grows faster than any computable functions, there have to be some statements that have very long proofs; and perhaps the four color theorem is one of them.

Ideas in Search of a Blog Post

I keep a list of ideas for blog posts, but some will never turn into posts. So here are a few random thoughts from that list.

• Some people like to write prose, some people like to write lists, like Bill's last post. Bill will often send me an email that's a list of items. I prefer the prose and usually avoid the lists with today being the "exception that proves the rule" (an expression that I never understood).
  
  I do have to admit that lists are very efficient, when I can respond to Bill like 
1. yes
2. no
3. Friday
4. Did you really expect happy comments on that post?
• Marissa Mayer has banned working at home for Yahoo employees. Lots of academics work at home when they aren't teaching. I didn't have any more deep insights here so it didn't become a post.
• I have a note to write a blog post on "confusing university names". I wonder what was confusing me.

I'll end this post of uninteresting post ideas with the wine tasting story. At Cornell there was a popular course on wine tasting open only to graduating seniors. Alas it conflicted with graduate complexity which I took from the great Juris Hartmanis. I don't regret that choice but missed the wine.

When I was a grad student at MIT there was a wine tasting course held during the short IAP session during winter break. So we took that course. A fun course. On the last day we all dressed up for the really fine wine. The instructor came to class in his tux even though he was quite ill that day. Two days later everyone in the class got sick as well.

There ought to be a moral to that story but I haven't figured it out yet. 

Oh, I remember/recorded/DVRed it well

You can now wear a device, Memoto that will take a picture every 30 seconds. Do you really have a Kodak Moment every 30 seconds? No, but this way when you do have one it will be captured (unless it happens at just the wrong time.) There is another one called Autographer which claims to be a "smart" camera that will take tons of pictures of your day. A photographer wore one and had his team all wearing them during a photo shoot.

Current historians who study ancient civilizations have the problem of very little being preserved. They go on whatever, perhaps by chance, happened to survive. King Tut is studied NOT because he was an important king, but because we have LOTS of his stuff. (What if America is destroyed and all that is left is the Gerald Ford Library?}

Future Historians may have the problem of having too much written down, recorded, emailed, blogged, tweeted. Or they may have the problem current historians have if some of these technologies go out-of-date so a lot is lost. Floppy's are already unreadable, Video Tapes and VCR's are degrading, beta-tapes--- as your grandparents what they were. They may also have the Galaxy Quest problem of mistaking our TV shows for historical documents (oh that poor Gilligan!).

What do we and don't we preserve?

1. Almost every TV show and Movie produced since DVDs came out, no matter how bad, is on DVD. Is there a directors cuts of Dude, where's my car?? Will future generations need that?
   
2. News shows are not preserved. Too bad- I might want a complete set of THE DAILY SHOW and THE COLBERT REPORT. Future historians may have the problem of mistaking these shows for satire.
   
3. Quiz shows are not preserved. Too bad- I liked BEAT THE GEEKS but all I have are some video tapes I recorded when it was on.
   
4. Sporting events- This is borderline since there are DVDs of past Superbowl's, World Series, etc, but not of ordinary games.
   
5. Many TV movies don't make it to DVD. Is that a loss?
   
6. Much TV from before the video tape age is lost. Some survives. It is somewhat arbitrary. I Love Lucy was done on some sort of medium that survived, others did not.
   
7. A very odd case: Dr. Who. There are rumors that some fans audiotaped the early episodes and that the only form in which they are preserved. See here, here.
   
8. Commercials. Aside from arbitrary things people happen to have taped, most commercials will not survive! What will future generations do without all of those insurance companies claiming that they are cheaper than the other ones?
   
9. What if the only knowledge of complexity theory that survives is Lance's book. That would be okay!
   
10. What if the only knowledge of complexity theory that survives are the Bill/Lance Podcasts. Hmm...
    

Quasi related to the theme of today's post (today's post has a theme?) is the question Who was the first married sitcom couple to be shown sleeping in the same bed? The funny answers are The Flintstones and The Munsters, indicating that America was so prudish they couldn't show real humans in bed. The first real-human couple is then said to be the Brady Bunch. But actually a couple named Mary Kay and Johnny from a sitcom in 1947 are said to be the first. The networks were less prudish because the couple really was married (also, TV was SO new back then). But here is my point- The show DOES NOT EXIST ON VIDEO TAPE OR DVD OR ANY MEDIUM. So the answer is only people's memories which could be faulty. We are already losing access to some TV trivia! Incidentally, are there any happily married couples on TV anymore? (The FBI agent on White Collar comes to mine, but nobody else.) (Added later: Our knowledge of TV trivia is actually increasing! see here.


What about journal articles? Do we do the future a DISservice by publishing too much and making it harder to find stuff? Or will they have the tools to find what they want? Today we have Google Scholar and some other tools- but are we putting all of our eggs in one basket? Will all of our papers survive or only the good ones? Or is every paper a gem worthy of preserving for future generations? While I doubt this is true, you never know when someone is going to need the Canonical a-ary Ramsey Theorem to prove something in geometry.

The Golden Ticket

Today is the official publication date of my first book The Golden Ticket: P, NP and the Search for the Impossible by Princeton University Press, though the book has been available on Amazon and in some bookstores for a couple of weeks now. This book takes a non-technical tour of our favorite open question through a series of stories and examples, covering P, NP, NP-complete, the "beautiful world" if P = NP, and how to deal with hard problems since we surely don't live in that world and a bit of history, cryptography and quantum. How "non-technical": I never actually define P and NP and avoid formulas and terminology except as needed to describe circuits and Cook's theorem.

I spent three years on this book project, building on my CACM survey. Thanks to all of you readers for your support, your suggestions for maps (some of which I used), titles and epigraphs (none of which I used).

You can keep up with all the happenings of the book on its own twitter and website.The Golden Ticket has already received some nice reviews. You can also check out an article I wrote for the Daily Dot and podcasts interview at  Wild About Math and the New Books Network. There are Japanese and Chinese translations in the works.

Hope you enjoy the book, recommend it all all your friends and help preach the gospel of P v NP.

Post Mortem on an April Fool's day joke

Recall that on April Fools Day I had a post about R(5) being discovered via a collaboration of Math and History. Many readers emailed me asking how many people were fooled (apparently they weren't!). I can't tell if it fooled ANY of my astute readers, though I hope it amused them. I CAN tell how many of my STUDENTS if fooled. I did an experiment on my class for which I CAN report the results.

1. All semester I gave would say things like there has been some progress on R(5), but I'll talk about that later
   
2. On March 28 I gave them my paper Ramsey Theory and the History of Pre-Christian England: An Example of Interdisciplinary Research and told them that I was going to do an experiment with the flipped classroom concept (this is Real educational thing)- they would read the paper, and on Tues Apr 2 I would give them a quiz on it (to make sure they read it) and we would discuss it.
   

I DID give them a quiz, but I asked them to NOT sign it so it was more of a survey. Here is a summary of the questions, the stats on it, and what to make of it. 17 people took the quiz (the class has 16 and some auditors.)

1. When did you Realize it was a hoax?
   
   1. When I first took this quiz: 5
      
   2. When I saw that Fifty shades of Grey was one of the references: 1
      
   3. When I went to the website that was supposed to have R(5) and it revealed the hoax: 3
      
   4. When I saw the name H.K. Donnut: 2
      
   5. When I read your April 1 blog: 1
      
   6. When I heard other students talk about it (though I kind of knew anyway): 4
      
   7. When I read the title: 1
      
   UPSHOT: I would count answers 1,2,3 as being fooled. So NINE were fooled. An earlier proofreader believed it because he wanted to so badly.
2. Was it okay to have you read a hoax paper? (NOTE: My wife thought NO.)
   
   1. This assignment was awesome!: 9
      
   2. Liked learning to not always belief a prof: 1 (When I tell him the Large Ramsey Theorem can't be prove in PA will he say That's bullshit man!):
      
   3. Assignment was okay (I could tell these people were not amused): 7
      
   4. Okay as far as it goes, but 10 pages! C'mon, that's too much: 1 (This is quite fair, but it was an easy read).
      
   UPSHOT: I all it a success!
3. Which of the names are Real and which did I make up?
   
   1. Eugene Wigner. REAL. Fake:4, Real:13. Name does sound funny.
      
   2. Herbert Scarf. REAL. Fake:9 Real:8. Real name that fooled the most people.
      
   3. Samuel Harrington. REAL. Fake:1 Real:16
      
   4. Dorwin Cartrwright. REAL. Fake: 6 Real: 11. I thought this would fool more people.
      
   5. Frank Harary. REAL. Fake: 3, Real: 14 (One thought I misspelled the real name. I didn't, but given my bad spelling, and the nature of the name, I can see why they thought so.)
      
   6. Charles Percy Snow. REAL. Fake: 5, Real: 12
      
   7. Jacob Fox. REAL. Fake:3, Real: 14. I've met him, he's real!
      
   8. Sandor Szalai. REAL. Fake: 4, Real: 13. Looks fake to me.
      
   9. Paul Erdos. REAL. Fake: 0, Real: 17. Seems like a mythical figure.
      
   10. Paul Turan. REAL. Fake: 3, Real: 14. One thought it was a play on Turing.
       
   11. Vera Sos. REAL. Fake: 3, Real: 14. I'm surprised people thought this name is real- I wouldn't have.
       
   12. Sir Woodson Kneading. FAKE- It's an anagram of Doris Kearns Goodwin, historian. Fake: 10, Real: 7. I'm amazed that 7 thought it was real.
       
   13. H.K. Donnut. FAKE- It's an anagram of Don Knuth. Fake: 13. Real: 4. Looks so fake it has to be Real? I was originally going to use Hal D.K. Donnut which is an anagram for Donald Knuth. I still don't know which looks more real.
       
   14. Moss Chill Beaches- FAKE- it's an anagram of Michael Beschloss, a presidential historian (He studies presidents, he is not, himself presidential). Fake: 13, Real: 4. My most fake looking name.
       
   15. Tim Andrer Grant- FAKE- It's an anagram of Martin Gardner. Fake: 5, Real:12. Tim is a reasonable first name, Grant is a reasonable last name, and Andrer--- well, middle names are sometimes weird.
       
   16. Alma Rho Grand- FAKE- It's an anagram of Ronald Graham. Fake: 14, Real: 3. My favorite fake name.
       
   17. D.H.J. Polymath- FAKE, but not my invention. It's used on the Polymath paper that proved the Density Hales Jewitt Theorem using elem methods (see here). Fake: 12, Real: 5. The people who thought it was real were either kidding OR read the question as a trick question Fake name that BILL MADE UP-- this is a fake name but BILL didn't make it up.
       
   18. Ana Writset- FAKE, It's an anagram of Ian Stewart. Fake: 4, Real: 13. Fake name that fooled the most people.
       
   19. Tee A. Cornet- FAKE- It's an anagram of Terence Tao. Fake: 8. Real:9. Is Tee anyone's first name?
       
   20. Andy Parrish- REAL. Fake: 1, Real: 16. I hope he's real, he's one of my proofreaders.
       
   21. Stephen Fenner- REAL. Fake: 1, Real: 16. I hope he's real- I taught him the construction of an r.e. minimal pair.
       
   22. Clyde Kruskal- REAL. Fake: 0, Real: 17. Real on a good day.
       
   One of the students who knew the Fake names were anagrams, and thought Dorwin Cartrwright was fake, spend an hour trying to find the anagram it was of. Can people spot fake names easily? I doubt it since many real names look fake, and many fake names look real. Along those lines, what do the stage names Clint Eastwood and Dolly Parton have in common? See here for the answer.
4. Speculate on how I came up with the false names. Most left this blank. Some said Anagrams, some mentioned anagram-programs on the web (I did use one), some said random-name-generator pointing out that Vera Sos and Sandor Szalai look like they were produced by a not-very-good random name generator.
   UPSHOT: As Blanch Nail Roam said You can fool some of the people all of the time, and all of the people some of the time, but you can't fool all of the people all of the time.
   

You should apply for STOC and/or CCC travel money (students)

Once again there is some money from ACM and from NSF for students to goto STOC, and I am the one to send the applications to. The link for info on how to apply is on the STOC webpage, but I give it here as well. Note that the deadline is April 16.

ALSO there is travel money for CCC: see here (though I am NOT the one to send applications for that one).

If you are a grad student going to STOC and CCC then you SHOULD apply for both. If you are a grad student going to STOC but NOT CCC then you SHOULD apply for STOC. If you are a grad student going to CCC but not STOC then you SHOULD apply for CCC. If you are a grad student going to neither then... well, I have no advice for you.

1. The application process is EASY.
   
2. Not that many have applied so you have a chance. But see next note.
   
3. THIS blog posting may make point 2 false.
   
4. For STOC it was only one applicant per advisor; however, we have RAISED it to TWO.
   
5. There is a priority for members of underrepresented groups. This DOES NOT just mean Women and minorities, it also means people from institutions that don't normally send students to STOC. However, you should APPLY even if you don't fit these descriptions.
   
6. We prefer people whose advisor don't have the money to send them, or are at least short on cold hard cash.
   
7. So what I really want you to is tell people who should want to go but either don't quite know what it is or don't have the money.
   
8. The above are only priorities. We want to support students as much as we can, so we will be spending money, not hoarding it. Even if you thing you have low priority for one of the reasons above, you should still apply. And again- APPLYING IS EASY.
   
9. The deadline is April 16, so get to it!
   

This also raises the question: SHOULD you goto STOC? YES

1. Even if you are a first year theory grad students its good to see whats out there.
   
2. Things you see may inspire you. My interest in Ramsey Theory came partially from seeing a STOC talk by Lipton or Chandra of Furst on bounds on Multiparty Comm Complexity that used the Gallai-Witt theorem
   
3. You get to meet people. Note that many of the people who proved basic theorems are still alive.
   
4. If you are work in complexity and also apply for the Student Travel Grant for CCC, and get both, you can goto BOTH!
   

Technology and Jobs

Entertainment Weekly reported last month on the bankruptcy of the special effects company Rhythm and Hues and the troubled industry. I remarked five years ago that the special effects industry lost its ability to surprise us. Without the ability to innovate, and with most of the effects handled in software, the need for specialized talent and companies disappears.

We've always could take comfort that computation and its related efficiencies have led to more, often safer and higher paying jobs. But is that still true? The stock market has hit historic highs but the unemployment rate remains high. Are companies who pared down during the last recession realizing they don't need to hire as the economy comes back?

Erik Brynjolfsson and Andrew McAfee in their 2012 book Race Against the Machine: How the Digital Revolution is Accelerating Innovation, Driving Productivity, and Irreversibly Transforming Employment and the Economy, argue that computer technology has truly gotten us to the point where we need fewer people to perform the task at the middle of the economy. The world needs computer scientists and welders, but far less people doing mid-level professional work. On the other side, Henrik Christensen, a Georgia Tech roboticist, argues that technology will continue to produce far more jobs than it displaces.

My take: It's just too early to tell. The economy could completely turn around and near full employment. Or we can see a permanent loss in returning jobs. History doesn't seem like a good guide here.

There are so many issues tied to the current state of employment and this sense of technological efficiency replacing jobs: Is college really worth the cost? Should an undergraduate student major in a STEM field or follow their passion if it lies elsewhere? Do we need MOOCs to improve access to quality education and/or keep down education costs? Are academics the next group to meet the efficiency maker?

My oldest daughter starts college next year and I don't even know what advice to give her.

Is the rule of threes a meta-urban legend?

Roger Ebert died on April 4, 2013. Margaret Thatcher died on April 8, 2013. I have heard the urban legend that celebrities die in threes.

1. Does anyone really believe this? Is it an urban legend that this is an urban legend?
   
2. YES- there was an episode of 30 Rock based on this.
   
3. NO- 30 Rock is FICTION.
   
4. Whenever I've seen ``examples'' of this at least one of the three isn't a celebrity. Are politicians really celebrities? For that matter, are Movie Critics really celebrities (Roger Ebert may qualify but very few others would.)
   
5. The notion of Celebrity is not well defined. People change it to make the rule-of-threes work. Can there be a rigorous definition of celebrity, perhaps based on the indegree of the I"VE HEARD OF THEM directed graph.
   
6. I predict that somebody marginally famous will die in the next few weeks and someone will say its the rule of threes. But will the person who says it be serious? And will the person who dies really be a celebrity (whatever that means)?
   
7. The paradox: there are so many famous people that I haven't heard of most of them.
   

I keep a list of old celebrities (defined as people that I have heard of-- websites of old celebrities have lots of people I never heard of) so that when they die I am NOT one of those saying I thought they were already dead. I noticed this when Dear Abby died: (1) young people asked Whose that? where as older people said I thought she was already dead. Margaret Thatcher and Roger Ebert people seemed to know they were alive.

Gary Miller to Receive the Knuth Prize

The 2013 Knuth Prize will be awarded to Gary Miller at STOC (ACM Press Release). The Knuth prize is now given yearly for outstanding contributions to the foundations of computer science, jointly sponsored by ACM SIGACT and the IEEE TC on Mathematical Foundations of Computer Science.

In 1975, Gary Miller gave a polynomial-time algorithm for primality assuming that the extended Riemann Hypothesis is true. For a given n, if there is an x and j such that x^2j mod n is not 1 or -1 and x^2j+1 mod n ≡ 1 then n can't be prime. Gary showed that ERH implied that if n is composite there must be such an x ≤ O(log² n). Given ERH one could just search all possible x and j in time polynomial in the number of bits to describe n.

Rabin noted that one could choose x at random to get a probabilistic algorithm that was correct with high confidence without any ERH assumption, now called the Miller-Rabin test. In 2002, Agrawal, Kayal and Saxena showed a polynomial-time algorithm for primality without assumption, but the Miller-Rabin test is still much faster in practice.

This is just part of Miller's contribution. From the press release:

Miller also made significant contributions to the theory of isomorphism testing—the problem of telling whether two structures are the same except for the labeling of their components.  He showed the equivalence of many different isomorphism problems to the still-open problem of graph isomorphism, and identified many special cases that could be solved efficiently. These included the problem of testing isomorphism for a special case known as bounded-genus graphs, a result he obtained with John Reif in 1980.  In 1985, in another collaboration with Reif, Miller invented the concept of "parallel tree contraction." This is one of the most fundamental primitives in parallel algorithm design with wide applications to graph theoretical and algebraic problems.

In 1984, Miller moved into the area of scientific computing. He set up the theoretical foundations for mesh generation, and was the first to design meshing algorithms with near-optimal runtime guarantees.  His subsequent research led to his breakthrough 2010 results with Ioannis Koutis and Richard Peng that currently provide the fastest algorithms—in theory and practice—for solving "symmetric diagonally dominant" linear systems. These systems have important applications in image processing, network algorithms, engineering, and physical simulations.  

Come to STOC and see Gary Miller's Knuth prize lecture. The program has just been posted and if you need financial help to attend, the student travel grant deadline is April 16.

A nice case of interdisciplinary research

(NOTE- this post is an April Fools Day post and is NOT TRUE. I a pointing this out since several people have read and and thought it was true and incorporated it into otherwise serious papers.)

All of the math and history in this post is elaborated on in my paper here.

Are there any interesting applications of PURE math to the Social Sciences or History? Scarf's application of the Brouwer fixed point theorem to Economics is one of many examples of applying (arguably) pure Mathematics to Economics. Cartwright, Harary, and others appear to have used graph theory to model social relationships; however, on closer inspection they just used the language of graph theory. In C.P. Snow's article, The Two Cultures, he speculates that there is a cultural divide between the sciences and the humanities, which may make such collaborations difficult. This points to the lack of interaction between the sciences and the humanities being a sociological problem in itself; however, we are not going to go there.

There was an application of Ramsey theory to sociology in the 1950's. In Jacob Fox's Lecture Notes in Combinatorics he tells the the following well known story:

In the 1950's, a Hungarian sociologist Sandor Szalai studied friendship relationships between children. He observed that in any group of around 20 children he was able to find four children who were mutual friends, or four children such that no two of them were friends. Before drawing any sociological conclusions, Szalai consulted three eminent mathematicians in Hungary at that time: Paul Erdos, Paul Turan, and Vera Sos. A brief discussion revealed that indeed this is a mathematical phenomenon rather than a sociological one. (Namely R(4)=18≤20.)

This is more of an anti-application since math was used to prove there was NO interesting sociology.


Recently there was a REAL application of Ramsey Theory to History, and later of History to Ramsey Theory. We summarize the results; however, the reader should look at the link above for more details.

1. Sir Woodson Kneading, a scholar of pre-christian history of England noted that, from 600BC to 400BC, whenever 6 lords were in close proximity, war broke out (with one exception). Either 3,4, or 5 of them formed an alliance against the rest, or 3,4,5, or 6 hated each other and went to war. The exception: all six formed an alliance. Kneading hired a CS grad student, H.K. Donnut, to verify the data. (Note that they really used R(3)=6.)
   
2. Kneading noted that, between 400BC and 200BC, whenever 18 lords were in close proximity, war broke out. Either 4,...,17 of them formed an alliance against the rest, or 4,...,18 hated each other and went to war. Again, Donnut verified the data (Note that they really used R(4)=18.)
   
3. Kneading found more results of this sort. His resuls and speculations, when translated to mathematics, are Ramsey Theoretic.
   
4. Kneading wrote a 300 page book on this topic using the data that he colleced and Donnut verified (Donnut declined to be a co-author since, in his view, Kneading did the intellectual heavy lifting).
   
5. Alma Rho Grand, a combinatorist, saw Kneading's book and realized that Ramsey Theory would simplify the work tremendously. Grand and Kneading wrote an article of which Kneading said My paper with Alma says cleanly in 30 pages what I said clumsily in 300 pages.
   
6. Grand noticed that one of Kneading's examples had 48 lords in proximity but no war broke out. This was in an era where if 5 formed an alliance or if 5 hated each other then a war should happen. She verified that this configuration showed R(5)≥49. It is already known that R(5) ≤ 49. Hence she showed R(5)=49. (Note that R(5) was unknown before this time.)
   

This is a case where Ramsey Theory helped History and History helped Ramsey Theory. Hopefully there will be more.
~