“Toward Mechanical Mathematics”, 1960 ():
The gallant tailor: 7 (flies) in one blow.
IBM 704: 220 theorems (in the propositional calculus) in 3 minutes.
[Some] results are reported here of a rather successful attempt of proving all theorems, totaling near 400, of Principia Mathematica [Wang emphasizes the improvement over Logic Theorist] which are strictly in the realm of logic, viz., the restricted predicate calculus with equality [in 37 minutes on an IBM 704]. A number of other problems of the same type are discussed.
It is suggested that the time is ripe for a new branch of applied logic which may be called “inferential” analysis, which treats proofs as numerical analysis does calculations. This discipline seems capable, in the not too remote future, of leading to machine proofs of difficult new theorems. An easier preparatory task is to use machines to formalize proofs of known theorems. This line of work may also lead to mechanical checks of new mathematical results comparable to the debugging of a program.
…We do not and cannot set out to settle all questions of a given domain, decidable or not, when, as is usually the case, the domain includes infinitely many particular questions. In addition, it is not widely realized how large the decidable subdomains of an undecidable domain (eg. the predicate calculus) are. Moreover, even in an undecidable area, the question of finding a proof for a proposition known to be a theorem, or formalizing a sketch into a detailed proof, is decidable theoretically. The state of affairs arising from the Godel incompleteness is even less relevant to the sort of work envisaged here. The purpose here is at most to prove mathematical theorems or the usual kind, eg. as exemplified by treatises on number theory, yet not a single “garden-variety” theorem of number theory has been found unprovable in the current axiom system of number theory. The concept of approximate proofs, though undeniably of a kind other than approximations in numerical calculations, is not incapable of more exact formulation in terms of, say, sketches of and gradual improvements toward a correct proof.
View PDF: