hi all! am pleased to write up a topic that Ive studied for decades and have recently collected many interesting & fascinating links from wideranging cybersurfing expedition(s): automated computer theorem proving (ATP) [c2] and the closely associated computer assisted proofs.[c1] the recent trigger/occasion for finally writing up this roaming reverie is a blog by fortnow [a2] mentioning the NYT article/obituary [a1] on Appel of Appel and Haken 1976 4-color [automated] theorem fame.[c3]
in my opinion [as a computer scientist] this is one of the great theorems of the 20th century, and I can vaguely recall reading inspiring science and even newspaper articles about the breakthrough when I was young. although alas, as Fortnow alludes in his questioning subtitle “still controversial?”, not all mathematicians are so impressed. some ambivalent and/or skeptical [hardcore?] naysayers still cite that it seems to be isolated and does not seem to be tied to other deep theorems as with important bridge theorems, or that with all the special cases and computer code is not humanly comprehensible or verifiable, [etc].
the proof has been worked on by others to simplify and streamline it eg Gonthier,[a3][a9] who, now working at Microsoft research, is one of the most prominent authorities in the field with other recent breakthroughs.[f6]
imho more than half of the great breakthrough of the proof was to reduce an infinite number of cases to a finite number of cases. this is related to a concept that the visionary Hilbert had of “finitistic” or “finitary” mathematics [c5] and which imho is still central yet mysterious and unexplored. computers can help with theorem proving but only after the problem is reduced to a finite number of cases (or, reducing a statement/property about infinite number of objects to a finite proof).
this basic operation or conceptual leap (“finitizing”?) must be happening in all nontrivial proofs but the way it happens in every different proof seems irregular, there does not seem to be a underlying pattern that Hilbert was grasping for over a century ago—and of course both Turing’s & Gödel’s famous proofs of undecidability prove that such a hunt is inherently quixotic and somewhat chimerical; although there could be a sly “loophole”.[i4][a5]
there are some outstanding online resources/refs on the subject of ATP. eg, special issue in Notices AMS [a4] and a relatively recent glowing Simons article/profile.[b4] another closely related area is “proving program termination” recently profiled in ACM.[a5] the results in the field of ATP are occasionaly dramatic and the overall field is attractive, trendy, even at times quite cutting-edge and exciting, inspiring amusing/clever parody.[b5]
this is a deep connection between software and mathematics that is not totally appreciated by everybody to date. it was 1st observed long ago with the Curry Howard correspondence.[c4] the basic idea is that proofs and programs have a remarkable correspondence. its very technical, but briefly, a lemma is like a subroutine, and a theorem is like or similar to a program that runs verifying some particular property. also, there are many proofs that are like a program that runs infinitely long and verifies some property for every case, and halts if the verification fails, showing a link to the area of program termination.
there are some old breakthroughs in ATP eg the robbins proof from boolean algebras, profiled in NYT.[b1] also just saw a big milestone of the Myhill Nerode theorem for FSMs [b2] which has strong connections to FSM optimization/minimization. another neat reference is the formalization of Godel’s theorem in ATP software by Shankar.[b3] another eminent/pioneering/forerunning authority and near-contrarian Zeilberger has been advocating automated proofs for many years and just got major recent recognition.[b4] another huge breakthrough was the Kepler conjecture ATP by Hales in 1997 [c6] which is actually more than ¼-century older than Fermats Last Theorem [itself 3½-century old!] and arguably far much more important than FLT or the 4-color theorem!
combinatorics — while delving deeply into this subject, the topic’s deep connection to combinatorics and another old controversy [amazingly, still active!] started to pop out. combinatorics proofs, working with discrete objects, are apparently more naturally amenable to computer proofs. discrete mathematics and combinatorics are definitely highly intimate to the point of being almost married with computer science. but, combinatorics surprisingly is a relatively recent mathematical invention! [a6] is a nice recent survey.
that did not occur to me when I started studying the subject when it was already decades old, but the pioneers of the field are still alive and remember vividly a time when it was groundbreaking and yet not so popular, see eg preeminent forerunner/pioneer/authority Lovasz [a8] describing this in a video interview with Widgerson.[a7] mathematicians sometimes have very long views of history and we computer scientists should realize in the long view scheme of things we are mere upstarts!
this culminates in a hilarious off-the-record, yet apparently genuine quote [a6] that is about the closest an elite mathematician—who normally inhabit a rarified, genteel, discreet realm—can come to outright “trash talk”:
Combinatorics is the slums of topology. —Whitehead
* * *
recently I have been very fascinated & near excited over WT Gowers blog directions in this area.[d1-5] I found the blog recently and in it a huge raging controversy in his latest comment threads over the win by Szeremerdi of the Abel prize (which indeed can be viewed as a dramatic combinatorics vs analysis “upset”). maybe the intense controversy is due to the very high award of $1M which is a big deal in math, where for many years the most prestigious prize of the Fields medal only awarded ~$15K! but most of the commotion is singlehandedly caused by a particular
troll commenter named “sowa” and everyones reaction to his near-rantings.
“sowa” is quite a colorful character! clearly intelligent and articulate, and yet at times bordering on a cartoonish 1-d charicature, a cranky curmudgeon, he has created his own blog entitled “stop timothy gowers” over a year ago.[e1-5] mainly it seems in reactionary complaint to Gower’s purported/supposed [hidden?] influence on the selection of Szemeredi, whose chief mathematical contributions are in combinatorics, which [in misc vernacular, stackexchange or cyber parlance] sowa “disses” and feels should be “ghettoized”. what is surprising is how many mathematicians might [covertly!] have some sympathy for his views. the jury is out on who sowa is but he seems to be an accomplished Russian mathematician with a lot of strong opinions, many of them downplaying, devaluing, or rejecting the importance of combinatorics.
Gowers pulled quite a remarkable scientific near-prank right around april fools day, somewhat reminiscent of Milgrams old famous boundary-pushing sociological experiments! he put together some proofs on his web page and then asked respondents if they were “clear or unclear”. what he didnt mention was that some were [really!] computer-generated via some of his new software and a collaboration with a computer scientist!
the remarkable experiment is captured in several recent blog posts,[d1-d3] and there was high polling participation due to the experiment being profiled on HackerNews. (HackerNews also led to my highest daily spike in hits due to publicity over Fukuyama’s proof.) the computer-generated proofs did fool some experts who were sure they were human generated when they were computer generated (or vice versa). so, a sophisticated 21st century mathematical variation on the Turing test.
the overall program fits in with some of Gowers older published ideas. Gowers has two remarkable and influential essays on mathematics. in [d5] he talks about the “two cultures of mathematics” mainly [roughly boiled down to] the problem solvers vs. the problem conceptualizers (or problem solvers vs theory-builders, or roughly bottom-up vs top-down, respectively). the conceptualizers tend to correspond more with topological and continuous mathematics and the problem solvers more with discrete math and combinatorics experts. in [d4] (unfortunately only online in .ps format) he imagines a futuristic sci-fi scenario [another normally fringe/unconservative area for a mathematician!] where a human works in conjunction with a computer in an expert collaboration/dialog.
so the semi-debate between Gowers and his apparent archnemesis “shadow” sowa (Gowers is mostly refusing to take the bait) is entertaining, quasi-epic, and ongoing in cyberspace. last I checked, sowa was apparently stunned into total silence (a rare feat for hard core cyber trolls) and had absolutely zero response to Gowers bold, groundbreaking, maybe seminal new experiment and directions. Fields medalist Gowers collaboration with a computer scientist in the field of automated theorem proving is a striking new advance in the field, sure to make waves and further reactions.
in later sections Ive collected the many stackexchange [g] and mathoverflow [h] questions related to the area that Ive found, showing a very strong and widespread degree of public interest in the subject, including from computer science.[f,i]
have much more to say on the subject but for now will just “plug” my other recent effort, a brief writeup of an empirical attack on the Collatz conjecture based on FSM transducers.
- 1 Kenneth I. Appel, Mathematician Who Harnessed Computer Power, Is Dead at 80 – NYTimes.com
- 2 Computational Complexity: Computer Assisted Proofs- still controversial?
- 3 A computer-checked proof of the four color theorem — Georges Gonthier, Microsoft Research
- 4 Notices of the American Mathematical Society — A Special Issue on Formal Proof
- 5 Proving Program Termination | May 2011 | Communications of the ACM
- 6 Combinatorics entering the third millennium – Peter J. Cameron
- 7 László Lovász video interview | Simons Foundation
- 8 László Lovász biography | Simons Foundation
- 9 Formal Proof—The FourColor Theorem, Georges Gonthier, Notices AMS, 2008
- 1 With Major Math Proof, Brute Computers Show Flash of Reasoning Power – New York Times
- 2 A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions
- 3 Amazon.com: Metamathematics, Machines and Gödel’s Proof (Cambridge Tracts in Theoretical Computer Science) (9780521585330): N. Shankar: Books
- 4 In Computers We Trust? As math grows ever more complex, will computers reign? | Simons Foundation
- 5 Automatic Proof for Reimann’s Hypothesis? | Turing’s Invisible Hand
- 1 Computer-assisted proof – Wikipedia, the free encyclopedia
- 2 Automated theorem proving – Wikipedia, the free encyclopedia
- 3 Four color theorem – Wikipedia, the free encyclopedia
- 4 Curry–Howard correspondence – Wikipedia, the free encyclopedia
- 5 Finitism – Wikipedia, the free encyclopedia
- 6 Kepler sphere packing conjecture, Wikipedia
- 1 An experiment concerning mathematical writing | Gowers’s Weblog
- 2 A second experiment concerning mathematical writing. | Gowers’s Weblog
- 3 Answers, results of polls, and a brief description of the program | Gowers’s Weblog
- 4 Rough Structure and Classification – Springer
- 5 The Two Cultures of Mathematics — W.T. Gowers
- 1 Stop Timothy Gowers! !!!: D. Zeilberger’s Opinions 1 and 62
- 2 Stop Timothy Gowers! !!!: What is mathematics?
- 3 Stop Timothy Gowers! !!!: Combinatorics is not a new way of looking at mathematics
- 4 Stop Timothy Gowers! !!!: T. Gowers about replacing mathematicians by computers. 1
- 5 Stop Timothy Gowers! !!!: T. Gowers about replacing mathematicians by computers. 2
- 1 proofs – Where and how did computers help prove a theorem? – Theoretical Computer Science
- 2 automated theorem proving – Why is it so difficult for a computer to prove something? – Theoretical Computer Science
- 3 reference request – Automated theorem proving via unsupervised approaches – Theoretical Computer Science
- 4 lo.logic – Is there a reasonable automated proof system for TCS theorems? – Theoretical Computer Science Stack Exchange
- 5 lo.logic – What is the difference between proofs and programs (or between propositions and types)? – Theoretical Computer Science Stack Exchange
- 6 lo.logic – Interesting algorithms in the formalization of the Feit-Thompson theorem? – Theoretical Computer Science Stack Exchange
- 7 co.combinatorics – Why can machine learning not recognize prime numbers? – Theoretical Computer Science Stack Exchange
- 1 soft question – How to start with automated theorem proving? – Mathematics Stack Exchange
- 2 soft question – Has any previously unknown result been proven by an automated theorem prover? – Mathematics Stack Exchange
- 3 logic – What are the theorems of mathematics proved by a computer so far? – Mathematics Stack Exchange
- 4 Are computers going to be able to discover and prove important mathematics theorems? – Mathematics Stack Exchange
- 5 philosophy – Could computers someday discover theorems or find demonstrations? – Mathematics Stack Exchange
- 6 Is there an automated way to prove really boring elementary number theoretic results? – Mathematics Stack Exchange
- 7 What am I losing if I decide to perform all math by computer?
- 1 Reasons for success in automated theorem proving – MathOverflow
- 2 Intro to automatic theorem proving / logical foundations? – MathOverflow
- 3 Why is it so difficult to write complete (computer verifiable) proofs? – MathOverflow
- 4 Proof assistants for mathematics – MathOverflow
- 5 Interesting conjectures “discovered” by computers and proved by humans? – MathOverflow
- 6 Proof formalization
- 7 is there any proof assistant based on first order logic?
- 1 logic – Why do some inference engines need human assistance while others don’t? – Computer Science Stack Exchange
- 2 logic – Types of Automated Theorem Provers – Computer Science Stack Exchange
- 3 logic – Learning Automated Theorem Proving – Computer Science Stack Exchange
- 4 computability – Algorithm to solve Turing’s “Halting problem” – Computer Science Beta – Stack Exchange
- 5 is there a repository for the hierarchy of proofs?