Re: COMP: AI and mathematics: Proofs

From: Lee Daniel Crocker (
Date: Sat Jul 22 2000 - 01:12:09 MDT

> In a discussion in another forum, the question of whether computers have
> "found" valid mathematical proofs has come up. Being mathematically stunted,
> I thought I'd do a hand-off of the question to this forum, since someone able
> to comment intelligently on the question probably inhabits this forum. Any
> leads or help?

The scare quotes seem appropriate, because it really depends on what you
mean by "found". After all, humans programmed systems to search for
proofs, and generally directed them in what to look for, so I'd be more
inclined to say that human mathematicians found the proofs with the aid
of a computer (and which they would not have found without such aid).
The classic case is the four-color threorem: a computer was used to
enumerate and evaluate a large collection of maps, and then prove by
time-consuming brute force that a specific subset of the ones generated
exhausted all relevant possibilities. A human could not have done this
within a lifetime.

Similar programs have also "found" interesting theorems and their
proofs, given sufficient guidance from human programmers as to what
is "interesting", without specifically being told what to look for.

Lee Daniel Crocker <> <>
"All inventions or works of authorship original to me, herein and past,
are placed irrevocably in the public domain, and may be used or modified
for any purpose, without permission, attribution, or notification."--LDC

This archive was generated by hypermail 2b29 : Mon Oct 02 2000 - 17:35:04 MDT