adventures and commotions in automated theorem proving

2 Replies

math-calculator-robothi 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.

a. proof

b. milestones

c. wikipedia

d. gowers

e. sowa

f. cstheory

g. mathematics

h. mathoverflow

i. cs

2 thoughts on “adventures and commotions in automated theorem proving”

  1. Pingback: the joy of (cyber) mathematics | Turing Machine

  2. Pingback: select refs and big tribute to empirical CS/ math | Turing Machine

Leave a comment