Surely You Are Joking?
A new way to write mathematics
Vladimir Voevodsky won the Fields Medal in 2002 for his work on homotopy theory of algebraic varieties. Using his pioneering methods he proved, among many other things, a deep conjecture of John Milnor, that had been open for decades.
Today I want to talk about, no, rant about, a recent “breakthrough” that was just announced on the ACM Tech news service.
Every few days the ACM sends out a collection of breaking news that relates in various way to computing. Some of the stories are interesting, some are surprising, some are relatively mundane. Clearly ACM is under pressure to publish a list of stories every few days. They do this whether the stories are really breakthroughs or not—although the titles are always exciting.
Here is the list that I was looking at the other day.
- Detroit, Embracing New Auto Technologies, Seeks App Builders
- MIT Researchers Can See Through Walls Using “Wi-Vi”
- Siri’s Creators Demonstrate an Assistant That Takes the Initiative
- Feature Stops Apps From Stealing Phone Users’ Passwords
- SDN Awards Seek University, Research Potential
- NSF and Mozilla Announce Breakthrough Applications on a Faster, Smarter Internet of the Future
- Mathematicians Think Like Machines for Perfect Proofs
- Artificial Intellience in Mental Healthcare
- Visual Language Will Result in Better Services
- The Tao of Facebook: ‘Social Graph’ Takes New Path
- New Study Suggests Voynich Text Is Not a Hoax
- Google Creates Developers Cloud Playground for Code Testing
The stories all sounded interesting—some more than others—but one jumped out and got my immediate attention. Let’s look at the story:
Mathematicians Think Like Machines for Perfect Proofs
I have strong opinions about the words “perfect proofs.” Indeed.
Here is the story in detail, quoting from ACM’s digest of the article “Mathematicians Think Like Machines for Perfect Proofs” by Jacob Aron in the June 25th issue of the New Scientist.
A team of mathematicians led by Vladimir Voevodsky with Princeton’s Institute for Advanced Study have devised a new mathematical framework that forces people to think more like machines to check perfect proofs in collaboration with computers. The team’s manual explains the use of type theory as an alternative mathematical basis. Type theory stipulates that all proofs must describe how to mathematically construct the object they concern, which is the opposite of set theory. Once mathematicians have completed this task, their proof would automatically be supported by unshakable computational checks. It is impossible to write an incorrect proof, assuming the underlying code is defect-free, along with the automated proof assistants that verify everything as the mathematician goes along. Voevodsky’s team also says it is far easier to check the code than the entire proof in most instances. Not only does the new framework make proof-checking easier, it also is a move toward computers that one day could execute mathematics by themselves, which might potentially clear a path toward more advanced forms of artificial intelligence (AI). “My expectation is that all these separate, limited AI successes, like driving a car and playing chess, will eventually converge back, and then we’re going to get computers that are really very powerful,” says project collaborator Andrej Bauer.
The article says more:
Take the case of the 500-page proof of the long-standing abc conjecture published by Shinichi Mochizuki of Kyoto University in Japan last year. Nine months on, his colleagues still have no idea whether it is correct.
“That is an excellent example of a proof where a serious mathematician produces something that is very hard to understand,” says Bauer. “If mathematicians always proved things with computers, there would be no question whether there is a mistake.”
Voevodsky and his colleagues have created a new approach which is explained in their 600 page book.
To start, let me say that stipulating what a proof really is, to a Fields Medalist no less, is the exact definition to hubris. How can we even dream of saying something to such an expert on proofs? But art critics are allowed to say things about art, or movie critics about movies, well you get the point.
I also think that Voevodsky might not even disagree, but whether he does is immaterial. I feel compelled to say something about not his work, but the New Scientist article. The article is at best in my opinion misleading.
The burning issue in proofs is not in checking them. The main issue is in understanding them. The whole point of a proof is missed by this article. Completely missed. Not even close. Not even in the same universe we live in. Did I say off the mark?
A proof is not like an accounting audit that checks that two tables of numbers add up to the same tally. It is not something that just checks the “correctness” of a statement. A proof must supply insight. It must explain why something is true. It must be able to impart to the reader understanding about the math objects, and must explain.
Ken has also heard buzz about the book. But he recalls a conversation he had with Robin Milner in 1994. Ken asked how long it would be before mathematical proof systems could automate the kind of correctness proofs for context-free grammars he was teaching in undergraduate intro theory courses. Milner replied to Ken’s surprise,
“About 50 years.”
Ken adds that one measure being discussed about chess cheating is asking players to explain the strategies they had during the games. That is to say, a computer analysis printout might be a “proof” of a move being best, but if you the human cannot explain the thinking, it’s not yours.
We understand proofs—short or long—by many mechanisms. Yes people do check them. Here are some of the methods that are used:
Read the proof: We do read proofs. We do check them. Some proofs, even of open problems, can be checked very quickly. David Barrington’s beautiful result on bounded-width computation comes to mind. I heard about the proof by phone, and was quickly able to see that it was correct.
Explain the proof: We often explain the proof to others. This can be in a class, in a seminar, or in writing. The ability to explain the proof is one of the best ways I believe to be really sure that one understands the proof. I cannot count the number of times that I thought I had proved something, only to discover on explaining it to a colleague that my “proof” was wrong.
The world expert on explaining proofs is perhaps Terry Tao. In his blog and more in his excellent books he has the ability to explain the most complex theorems in ways that lay bare the critical insights. His approach is the exact opposite of that of “perfect proofs.” A typical explanation of his might go like: The general case is really not much different than the case where so we will assume that. Then we note that
Here is an example of this by Voevodsky himself on his own work.
Find a new proof: We often find new proofs of a theorem. The new proof can give additional insight in why the result is correct. Note this is not the same as checking the tally of the numbers again. A new proof to be “new” must prove the result in a substantially new way. The famous Quadratic Residue Theorem is a perfect example of this. Carl Gauss first proved it, but later published six proofs and two more were found after he died in his papers. Today there are over 200 published proofs, according to our friends at Wikipedia.
Use the proof: This means to actually use the theorem proved to do something. A simple example is Fermat’s Little Theorem. Recall this says that
for all primes and all relatively prime to . This theorem is used millions of times per day by the famous RSA encryption method. If there was some problem with the Fermat’s Theorem companies on the Internet using RSA would get grabbled messages. Since they do not, this is nice evidence that it really works
Use the theorem: We check theorems best, in my opinion, by using them to prove other results. As a theorem gets used more and more it is really being checked. I think that this is one of the best tests that it is correct. Who would doubt the Fundamental Theorem Of Arithmetic—the integers have unique factorization—now after countless applications?
Extend the theorem: We also check theorems by extending them. Fermat’s Little Theorem is extended to
for all and all relatively prime to , where is Leonhard Euler’s function. Even this could be further extended to
where is the Carmichael function—see here. More on Robert Carmichael, the inventor of this function, in a discussion I am working on right now.
Use the proof methods to prove new theorems: We also check proofs by using them methods in them to prove new theorems. One of the deepest examples of this might be Andrew Wiles 1995 proof of Fermat’s Last Theorem. He proved the so-called modularity theorem for semistable elliptic curves. Later in 1998 the full modularity theorem was proven by Christophe Breuil, Brian Conrad, Fred Diamond, and Richard Taylor. It used and built on the methods found in Wiles’ original proof. See here for details.
Here are the movies that were embedded by title or quote into our July 4th post—it is possible there were some we didn’t notice.
- “Liars” quote from The Oxford Murders;
- “Handle the truth” quote from A Few Good Men;
- Lost in Translation;
- Nobody’s Perfect;
- Double Trouble;
- Triple Trouble;
- The 39 Steps;
- The Right Stuff;
- There’s Something About Mary;
- The Statement;
- Only the Strong;
- In the Line of Fire;
- “Que Será, Será” quote from The Man Who Knew Too Much;
- Nothing in Common;
- The New World;
- Rules of Engagement;
- The World is Not Enough;
- Over the Top;
- Easy Living;
- Nowhere to Hide;
- Anything Else;
- The Delta Force;
- The Power of One;
- Big Fish;
- “Need for Speed” quote from Top Gun;
- Rear Window;
- How Stella Got Her Groove Back;
- “Badges” quote from The Treasure of the Sierra Madre (rather than from Blazing Saddles);
- Friday After Next.
Ken and I hope you liked the movie game.
For proofs a very neat page to read is this. It contains a history of some famous “proofs”: some were incomplete, some were fixed later, and some were just plain incorrect. What does this say about “what is a proof”?