Automated Theorem Proving

April 5, 2007

Posted by David Corfield

$MathML-enabled post (click for more details).$

In Brussels, we heard from Koen Vervloesem about attempts towards better automated theorem provers. Readers of my book will know that I devoted its second chapter to automated theorem provers, to provide a relief against which to consider ‘real mathematics’. One proof I focused on was that discovered by the program EQP for the Robbins problem. Where many would see the proof as a meaningless manipulation of symbols, Louis Kauffman was sufficiently impressed to say:

I understood EQP’s proof with an enjoyment that was very much the same as the enjoyment that I get from a proof produced by a human being.

Having not looked at automated theorem proving for a number of years, it was interesting to hear from Koen what has been happening. One crucial realisation was that computers would have to be given the capability to combine logical reasoning with algebraic manipulation. Trying to expand $(x + y)^2$ takes an inordinate amount of logical shuffling.

We heard about Michael Beeson’s Automatic generation of a proof of the irrationality of $e$ , Journal of Symbolic Computation 32, No. 4 (2001), pp. 333-349, which does manage this combination. Beeson may be better known to readers as a constructivist mathematician, but then perhaps the jump to automated theorem proving is not so surprising.

Always in these cases one looks to see how firmly the computer’s hand has been held. Naturally, we’re not expecting the machine to know why it matters whether a number is algebraic or not. Nor do we just feed in a definition of an algebraic number and expect it to cope. The task it is set is to show that:

$q \gt 0 \to \exists C(\mid\frac{p}{q} - e \mid \ge C/q! \gt 0)$

This is a condition which transcendental numbers satisfy. I’ll leave you to work out how impressed to be.

Posted at April 5, 2007 12:13 PM UTC

TrackBack URL for this Entry: https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1229

25 Comments & 1 Trackback

Read the post Over Munduruku, axiomatische methodes en unificering
Weblog: Filosofie voor elke dag
Excerpt: Zoals beloofd hier een korte bespreking van een aantal lezingen tijdens de Perspectives on Mathematical Practices 2007 conferentie. Het is onmogelijk om over alle lezingen iets te zeggen, want het was een druk programma. Vandaar dat ik hier de voor mij in
Tracked: April 5, 2007 3:02 PM

Re: Automated Theorem Proving

Well, there are those of us who use automated theorem provers, but don’t hold the computer’s hand to make them prove known results or to win competitions. Rather we use them in our research to discover new results.

I work quite a bit in the area of quasigroups and loops. I use Prover9, the successor to Otter developed by William McCune. My collaborators and I have used both Otter and Prover9 to solve some longstanding problems in the field.

To me, an important part of the process is “humanizing” the automated proof, that is, translating it into a form comprehensible by humans. This involves poring over the proof line by line, usually starting from the end. As I am reading it, I’ll come across a clause and think “Oh, that one follows immediately from such-and-such, so I don’t need to read Prover9’s proof”.

To give a concrete example, suppose I have managed to get Prover9 to prove something about Moufang loops. Such loops are diassociative, that is, any subloop generated by no more than two elements is associative. So if I am reading a proof and come across a two-variable instance of associativity, I don’t have to bother checking the proof of that particular clause. More generally, if the class of loops I am working on has known structure, I can use that in the translation process.

Eventually, with enough patience, I can get a proof that is not only checkable by humans (as any proof generated by this kind of software is, at least in principle), but is, in fact, comprehensible.

It is funny to use the word “reduce” here, but I like to think of it as “reducing” an entirely equational or first-order proof to higher order concepts. But occasionally there will be some part of a proof where it just isn’t possible to pull higher-order stuff out of a hat to get the result. In those cases, the best one can hope for is to write the steps as cleanly as possible. For instance, in our proof that every diassociative A-loop is Moufang, there is a lemma whose proof is just based on manipulating identities. It is a proof I still think it highly unlikely a human would have found (and certainly no human had in the 44 years the problem was open).

Posted by: Michael Kinyon on April 5, 2007 3:23 PM | Permalink | Reply to this

Re: Automated Theorem Proving

I guess a point that’s going to occur to some people, whether or not they’re impolite enough to raise it, goes something like the following.

To the extent that automated theorem provers have discovered anything new it’s in fields where, deprived of much by way of intuition or connection to other fields, it’s not so surprising that a combinatorial search picks up some unknown things. But chances are, nothing very important will be found.

Then they might quote Terence Tao:

the very best examples of good mathematics do not merely fulfil one or more of the criteria of mathematical quality listed at the beginning of the article, but are more importantly part of a greater mathematical story, which then unfurls to generate many further pieces of good mathematics of many different types. Indeed, one can view the history of entire fields of mathematics as being primarily generated by a handful of these great stories, their evolution through time, and their interaction with each other. I would thus conclude that good mathematics is not merely measured by one or more of the “local” qualities listed previously (though these are certainly important, and worth pursuing and debating), but also depends on the more “global” question of how it fits with other pieces of good mathematics, either by building upon earlier achievements or encouraging the development of future breakthroughs.

They might continue, Moufang loops and quasigroups/loops just aren’t going to appear in that ‘good’ mathematics, even if the nonzero octonions do form a Moufang loop. They’re just not part of any good story.

How might one respond to that point?

Posted by: David Corfield on April 5, 2007 4:20 PM | Permalink | Reply to this

Re: Automated Theorem Proving

They might continue, Moufang loops and quasigroups/loops just aren’t going to appear in that ‘good’ mathematics, even if the nonzero octonions do form a Moufang loop. They’re just not part of any good story.

How might one respond to that point?

Clearly (w)racks aren’t part of any good story, even if the conjugation action of a group on itself forms a rack. Except then it turns out they are.

Just because you haven’t read (or told!) the right stories yet doesn’t mean this or that trope isn’t part of a good story.

Posted by: John Armstrong on April 5, 2007 5:26 PM | Permalink | Reply to this

Re: Automated Theorem Proving

And that brings us back to Rota:

What can you prove with exterior algebra that you cannot prove without it?” Whenever you hear this question raised about some new piece of mathematics, be assured that you are likely to be in the presence of something important. In my time, I have heard it repeated for random variables, Laurent Schwartz’ theory of distributions, ideles and Grothendieck’s schemes, to mention only a few. A proper retort might be: “You are right. There is nothing in yesterday’s mathematics that could not also be proved without it. Exterior algebra is not meant to prove old facts, it is meant to disclose a new world. Disclosing new worlds is as worthwhile a mathematical enterprise as proving old conjectures. (Indiscrete Thoughts, 48)

But there must be times when a prescient mathematician judges correctly that some activity isn’t going anywhere interesting.

Posted by: David Corfield on April 5, 2007 6:22 PM | Permalink | Reply to this

Re: Automated Theorem Proving

I’m sure everyone reading this blog has had a colleague say the exact same thing about categories, let alone n-categories. I’m wondering, though, what it means when you have doubts in your own mind that what you’re working on is “anything but language”. I tend to run into that with most of my work, actually.

Posted by: John Armstrong on April 5, 2007 6:54 PM | Permalink | Reply to this

Re: Automated Theorem Proving

Perhaps it’s easier to start from the other end, when you know you’re onto something. Like Vaughan Jones must have felt when the connection to knots came up from his vN algebra work. Of course, people must make do with smaller encouragements.

Do we find cases of constructions later taken to be very important, which received none or few of these encouragements along the way?

Posted by: David Corfield on April 5, 2007 7:42 PM | Permalink | Reply to this

Louis Kauffman Re: Automated Theorem Proving

Which is exactly why Louis Kauffman’s comment is so interesting. Louis Kauffman has found – and proved – deep connections between Knot Theory, Logic, Philosophy, Polynomials, and Quantum Computing.

One of his papers on “imaginary logic” stimulated me to write about a 100 page draft paper on the subject, in the course of which it became clear to me that, despite having published before on Quantum Computing, I know next to nothing about it.

Posted by: Jonathan Vos Post on April 5, 2007 9:04 PM | Permalink | Reply to this

Re: Louis Kauffman Re: Automated Theorem Proving

Jonathan,

By imaginary logic are you talking about logics with values x such that x = not x? If you are, is your 100 page draft available online? It just dawned on me recently that there might be a nice interpretation of such logics.

Posted by: Dan Piponi on April 5, 2007 10:29 PM | Permalink | Reply to this

Let’s discuss offline; Re: Louis Kauffman Re: Automated Theorem Proving

Dear Dan Piponi,

Yes, per Kauffman and (decades earlier) Vasiliev. Draft paper can be emailed to you when I next find the diskette; not currently online; I am a great admirer of your graphics work, but do not know your email address. Mine is jvospost2@yahoo.com, and if you contact me, I’ll give you a less publically known edress. Little pieces of this draft paper have spun off to such venues as the Online Encyclopedia of Integer Sequences. I look forward to contact with you at your convenience.

Posted by: Jonathan Vos Post on April 7, 2007 8:44 PM | Permalink | Reply to this

Re: Automated Theorem Proving

Just a small remark on top of David’s: even if loops _are_ good for important things we’re unaware of, the fact most people _think_ they’re not leaves only a small number of people trying to solve the open problems, and thus makes it easier for machines to compete.

Posted by: Squark on April 5, 2007 7:53 PM | Permalink | Reply to this

Re: Automated Theorem Proving

A specific computational example and citations [Cawagas, R. E.] and [Hantao Zhang] is iven in:

http://www.research.att.com/~njas/sequences/A118641

Number of nonisomorphic finite invertible loops of order n.

n a(n)
5 1
6 33
7 2333

These are non-associative loops in which every element has a unique inverse and it includes IP, Moufang, and Bol loops [Cawagas]. The data were generated and checked by a supercomputer of 48 Pentium II 400 processors, specially built for automated reasoning, in about three days. In general, a loop is a quasigroup with an identity element e such that xe = x and ex = x for any x in the quasigroup. All groups are loops. A quasigroup is a groupoid G such that for all a and b in G, there exist unique c and d in G such that ac = b, and da = b. Hence a quasigroup is not required to have an identity element, nor be associative. Equivalently, one can state that quasigroups are precisely groupoids whose multiplication tables are Latin squares (possibly empty).

Posted by: Jonathan Vos Post on April 5, 2007 9:12 PM | Permalink | Reply to this

Re: Automated Theorem Proving

How might one respond to that point?

It’s not a point, it’s a multiplicity of comments.

I can’t speak for areas in which I don’t work, but the success of automated theorem proving in mine is not due to deprivation of intuition and certainly not to connection to other fields. (Most of us get into loop theory because of its intimate links to group theory.) It’s rather a function of the age of the subject and the number of people who have worked in it over the years. It’s an area in which there are problems that can still be formulated in ways in which a.t.p. can help. Group theory itself was once that way, of course, as a perusal of its history shows, but it matured and the open problems moved in a different direction.

It’s also not true that the success of a.t.p. in genuine mathematical research is largely combinatorial. Bob Veroff’s method of proof sketches shows that the structure of the problems themselves plays a large role.

I’ll ignore the remarks about “nothing important” or “good mathematics”. Such absolutism is indefensible.

An excellent example of this sort of thing of which I am sure you are all aware is the recent brouhaha with the Journal of the American Mathematical Society over the rejection of Fred Wehrung’s solution of the Dilworth Problem. The rejection, the full text of which is easily available, speaks not of the significance of the problem, nor of its connection to other fields (the solution uses set theory), but rather the usual process of marginalization.

Regarding ignorance of the story into which quasigroups and loops fit, I refer the hypothetical speaker to various sources, e.g., the Conway/Smith book or H.O. Pflugfelder’s Historical notes on loop theory, Comment. Math. Univ. Carolin. 41 (2000), no. 2, 359–370.

I realize you are just speaking hypothetically, David. Certainly, you are a defendant of an area (the subject of this blog) which is just as marginalized as MSC 20N05. Luckily, the area of n-categories has eloquent popularizers (JB) and those trying very hard to connect it to other areas (JB and urs).

Posted by: Michael Kinyon on April 5, 2007 9:04 PM | Permalink | Reply to this

Re: Automated Theorem Proving

Yes, I was speaking hypothetically. But I’m interested in where people place limits. On the face of it mathematics has the potential to be immensely broad. Those juicy parts that keep linking up in surprising ways seem to merit special attention. Is there anything which merits no attention?

If you search for ‘Smarandache’ and ‘neutrosophic’ on the ArXiv (even though the search facility there seems to have got a whole lot worse since they just ‘improved’ it), is that material worth supporting?

Posted by: David Corfield on April 5, 2007 9:28 PM | Permalink | Reply to this

Re: Automated Theorem Proving

On the face of it mathematics has the potential to be immensely broad.

Mathematics itself, yes, but mathematicians, rarely. The compartmentalization of knowledge seems to be an essential feature of human existence, and indeed, perhaps evolved as a survival mechanism. We understand some piece of mathematics very well, and the rest is just part of our web of belief, to use the Quinean term. If we are fortunate enough to be in a community with many others, than we will be able to establish connections to other parts of the web, and as part of our community formation process, we will be safe in referring to parts of the web far from us as being on the fringes.

is that material [Smarandache stuff] worth supporting?

That depends on your definition of “supporting”, but I would say “no”. I have my reasons, but you’re looking for general principles, and I have none to offer. I didn’t say I wasn’t as guilty of marginalization as anyone else, nor did I mean to imply that it is a sin.

Posted by: Michael Kinyon on April 5, 2007 10:24 PM | Permalink | Reply to this

Re: Automated Theorem Proving

$MathML-enabled post (click for more details).$

David wrote “They’re just not part of any good story. How might one respond to that point?” I know nothing about Moufang loops, but one response is that lots of mathematical activity has been initiated in an attempt to conquer a “pragmatic” issue and then someone has later found a compelling story to tell using those pieces. (To continue the literary analogy, it’s like an account published by someone involved in an important series of events: it’s only looking over the elements later that the patterns and threads become visible.)

To head back to maths, AIUI Fourier series were developed to approach heat conduction problems and subsequent developments made them central to a compelling, deep story about functions encompassing areas such as harmonic analysis, etc. I’m not a historian, but it’s unclear to me that at the time - particularly given the delay in giving convincing proofs of convergence - they wouldn’t have looked hyper-specialised. Likewise, I’ve read that in his later years other mathematicians wondered why Fourier was wasting time doing calculations on allocation problems that were viewed as “not proper mathematics”. It’s only in the twentieth century these things made connections to the interesting areas of algorithms, graph theory and constrained optimisation. I’d argue (and I know it’s controversial) that algorithms and optimisation are an interesting mathematical story, albeit one that has probably many fewer cross-connections with other stories than stories such as categorification, or group theory, etc. As another example, I understand the ideas developed in projective geometry for understanding perspective and plane geometry are widely used in other areas, but would the pioneers have seen anything beyond a narrow but important niche for what they were doing.

I wonder if a preoccupation with the mathematical story is a bit like “writing the great american novel”: the one way to guarantee you won’t is to set out deliberately to do it?

Posted by: dave tweed on April 5, 2007 9:48 PM | Permalink | Reply to this

Re: Automated Theorem Proving

It’s not so much a question of setting out to write a story, as the emphasis in the narration with hindsight is so often on surprise. E.g., who would have thought vN algebra towers would lead to knot invariants? Who would have thought that the drive to classify finite simple groups would end up with moonshine? Who would have thought that Brandt’s groupoids would turn out to offer us a way of mediating between Grothendieck’s and Connes’ notions of space?

Perhaps the latter example is less surprising. But why is surprise important in any case? When we later come to understand things well, we’ll probably be in a position to explain away what was a surprise, suggesting it’s just a state of ignorance.

I guess the answer must lie in what it is that can provide the checks on mathematical activity. Surprises give us a powerful sense that we’re not just pulling out rabbits we already placed in the hat.

Over here I likened the kinds of construction the categorification program expects to be possible, to prediction in science. We have Hopf algebras, there ought to be Hopf 2-algebras. But it’s not enough to say a sensible sounding definition is possible to find. It really had better do something unexpected.

Let’s hope John’s Tale of Groupoidification has some surprising twists and turns.

Posted by: David Corfield on April 6, 2007 8:01 AM | Permalink | Reply to this

Re: Automated Theorem Proving

$MathML-enabled post (click for more details).$

Another trite comment probably implicit in what you’re saying: the things that are mathematically compelling are often the things where there’s unexpectedly less going on than you’d initially expect, eg, you only have to add $i$ as the solution of $x^2=-1$ to $\mathbb{R}$ and complete to a field $\mathbb{C}$ to have all roots of all polynomials; you’d really expect to have to add lots of strange new entities with complicated interactions. For instance, I’ve been trying to get my head around “groupoids for partial symmetry” and so far I haven’t reached the point where I’ve thought “Oh, is that all there is going on? I thought it was going to be more involved”, which is a sign I haven’t really got the point yet. Indeed, I bet if you had a sophisticated natural language system to scan of the TWFs you’d find the equivalent sentiment cropping up relatively frequently.

Incidentally, just because it hasn’t been mentioned here, several of Zeilberger’s opinions are about why he thinks automated mathematics is real mathematics.

Posted by: dave tweed on April 6, 2007 10:20 AM | Permalink | Reply to this

Re: Automated Theorem Proving

Interesting your choice of the extension of the reals to the complex numbers. That was just the example André Joyal gave as an example of a mathematical miracle.

I mentioned Zeilberger’s opinions here. You can read a comment he made to my remark there too.

Posted by: David Corfield on April 6, 2007 10:44 AM | Permalink | Reply to this

Re: Automated Theorem Proving

$MathML-enabled post (click for more details).$

[…] vN algebra towers would lead to knot invariants

I have only a vague idea of what precisely you have in mind here. Could you point me to further details?

Probably this was discussed here recently, and I missed it.

I s vN algebra tower a chain of inclusions of subfactors?

Posted by: urs on April 7, 2007 1:29 PM | Permalink | Reply to this

Re: Automated Theorem Proving

I’m sure there must be acres of good exposition about this. Wikipedia has something on it in their subfactor entry.

Posted by: David Corfield on April 7, 2007 3:06 PM | Permalink | Reply to this

Re: Automated Theorem Proving

He’s referring to the Jones polynomial, in the original Jones setting.

Posted by: John Armstrong on April 7, 2007 4:45 PM | Permalink | Reply to this

Re: Automated Theorem Proving

I have an alternative explanation. Moufang loops and quasigroups are just too foreign to human experience for humans to prove theorems about them unaided. The most developed areas of algebra up to now are those where there is a notion of “representation theory”, a way to represent abstract objects (like groups) to concrete objects (like permutation groups and matrix groups). Now thanks to computers we will find a whole new rich world that was inaccessible to us because of our primitive mammalian brains.

I don’t know if I believe this, but it fits the observed facts.

Posted by: Walt on April 9, 2007 5:14 AM | Permalink | Reply to this

Re: Automated Theorem Proving

My M.S. in Computer and Information Sciences was for Automated Thereom Proving, back in 1975.

UNIVERSITY OF MASSACHUSETTS, Amherst, MA 1973-1975
M.S., Computers and Information Science (Artificial Intelligence)
* Designed and coded parallel automated theorem prover

My advisor (Daniel Fishman) had an existence proof in his PhD dissertation. In constructively found an alogorithm and data structure which did automated theorem proving much much faster than any system in the world at the time – according to our simulations. There were no Massively Parallel Procfessors available to us in 1975. Xerox made a commercial product from our system, without payment or acknowledgment. But it was great fun, anyay.

Please allow me to give an introductory description, for those new to this topic.

Practical Foundations of Mathematics
Paul Taylor

1.7 Automated Deduction

There are mechanised approaches to algebra,
combinatorics, numerical analysis, etc , but this book
is not about those subjects, it is about logic: all we
can discuss in this section is the choreography of [non-unicode characters], and reinforce the importance of the
scope of variables and hypotheses. We cannot do the
creative part of mathematics, because the solution to
a problem in number theory, for example, may be
“simply” an ingenious observation about z(s) = ån =
1¥ n-s or counting points in a cube in Rn.

The steps which can be automated are the obvious ones,
in a technical sense: this literally means “in the
way” in Latin. It is obvious how to go through a
foreign airport, not because you know it intimately,
but because there are signs telling you where to turn
whenever you need them (you hope). This is also known
as exam technique: write down and exploit what you
already know. Whereas the box or sequent rules of
predicate calculus from the previous section are the
laws of the game of proof, the heuristics are hints on
the tactics. This section is based on teaching first
year informatics students to construct proofs on
paper. Of course this will also give some idea of how
to write a program to do it, but the strategy for
making choices when backtracking is needed raises
issues far outside the scope of this book [Pau92].

George Polya [Pol45] and Imre Lakatos [ Lak63] gave
two classic accounts of heuristics in mathematics,
using Euclidean geometry for examples. Polya’s advice
- make a plan and carry it out, compare your problem
with known theorems, etc - is extremely valuable to
help students of mathematics (and professionals) get
past the blank sheet of paper, but treats more
strategic aspects of proof than we can. An early
theorem prover was based on his methods of drawing
diagrams and formulating conjectures and
counterexamples; that this seems odd now shows both
the sophistication of modern proof theory and perhaps
also the danger of isolation from the traditional
instincts of mathematicians.

Nikolas de Bruijn’s AUTOMATH project (late 1960s) set
out to codify existing mathematical arguments, rather
than to find new theorems, and this remains the
research objective of automated reasoning. Johan van
Benthem Jutting (1977) translated Edmund Landau’s book
Foundations of Analysis into AUTOMATH and analysed the
ratio by which the text is magnified, which was
approximately constant from beginning to end. Similar
work has been done for other areas of mathematics.

There are certain dangers inherent in the
formalisation of mathematics. Systems of axioms
acquire a certain sanctity with age, and in the how of
churning out theorems we forget why we were studying
these conditions in the first place. Computer
languages suffer far more from this problem: nobody
would claim any intrinsic merit for FORTRAN or HTML,
but sheer weight of existing code keeps them in use.
Through the need for a standard - any standard - a
similar disaster could befall mathematics if set
theory were chosen. As with any programming, and also
with the verification of programs, far more detail is
required than is customary in mathematics. G. H. Hardy
(1940) claimed that there is no permanent place in the
world for ugly mathematics, but I have never seen a
program which is not ugly. Even when the mathematical
context and formal language are clear, we should not
perpetuate old proofs but instead look for new and
more perspicuous ones.

===========

[dB80]
Nikolas de Bruijn. A survey of the project Automath.
In Curry et al. [CSH80], pages 579-606.

[CSH80]
Haskell Curry, Jonathan Seldin, and Roger Hindley,
editors. To H.B. Curry: Essays on Combinatory Logic,
Lambda Calculus and Formalism. Academic Press, 1980.

[Har40]
G. H. Hardy. A Mathematician’s Apology. Cambridge
University Press, 1940. Reprinted 1992.

[Lak63]
Imre Lakatos. Proofs and refutations: the logic of
mathematical discovery. British Journal for the
Philosophy of Science, 14:1-25, 1963. Edited by John
Worrall and Elie Zahar, Cambridge University Press,
1976.

[Pau92]
Lawrence Paulson. Designing a theorem prover. In
Samson Abramsky et al., editors, Handbook of Logic in
Computer Science, pages 415-475. Oxford University
Press, 1992.

[Pol45]
George Polya. How to Solve It: a New Aspect of
Mathematical Method. Princeton University Press, 1945.
Re- published by Penguin, 1990.

Posted by: Jonathan Vos Post on April 5, 2007 5:53 PM | Permalink | Reply to this

Computations and Automated Theorem Proving

There is a whole conference series dedicated to just this topic – see the (now unfunded) Calculemus Project. The next conference is (predictably) Calculemus 2007.

The central topic is how to get (automated) theorem proving systems (TP) and computer algebra systems (CAS) to (at least) talk to each other. Much to the surprise of most mathematicians, proving systems and computation systems have developed completely independently of each other over the last 30 years. The TP systems focused on logical rigor, which means that most of them are astonishingly slow, and all are quite hard to use. The computational systems are reasonably efficient, but bug-ridden, although feel easy to use.

Amusingly, I am co-author of a paper (accepted at Calculemus 2007) formally documenting a system which combines TP and CAS (and other like systems) to automatically discover identities for loops and quasi-groups! Formalizing such a system is quite challenging, as it needs to deal with theory, meta-theory and (gasp) a little meta-meta-theory. It also involves different logics (first-order and various conservative extensions for the theory, higher-order for the meta-theory, and we use STTwU for meta-meta).

Posted by: Jacques Carette on April 6, 2007 1:00 AM | Permalink | Reply to this

Re: Automated Theorem Proving

$MathML-enabled post (click for more details).$

Curious that a new proof of the irrationality of $e$ should appear within 5 days of my post.

Posted by: David Corfield on April 11, 2007 10:58 AM | Permalink | Reply to this

The n-Category Café

Skip to the Main Content

April 5, 2007