Geometric proof and discovery: human and artificial intelligence

Can a computer discover a mathematical theorem that impresses human mathematicians as beautiful and interesting? Can a computer prove a theorem in a way that human mathematicians would have difficulty following? The project aims to investigate these questions, in the specific domain of euclidean geometry. Euclid's axioms remain cornerstones of mathematical thought, and the geometry of two and three dimensions is still actively researched today. Since the 1950's, it has been known that --- in principle --- the process of discovering and proving theorems of euclidean geometry could be automated. But the gap between principle and practice remains considerable. Though they are ubiquitous in numerical computation and statistical data processing, computers have found very limited success as theorem-proving devices. This contest of the human vs. machine brain is rather similar to that in chess, where, until the 1990's, grandmaster-level play seemed to be the exclusive domain of human intelligence. The appearance of Deep Blue and its defeat of Kasparov, the standing world champion, led to a radical reevaluation of what machines can and cannot do. This project argues that, thanks to advances in hardware and algorithmic algebra, a similar breakthrough is possible in geometric theorem proving. The investigators will create software to comb through euclidean configurations and check whether a universally valid statement, i.e. a theorem of plane geometry has been found. (A "configuration" is a collection of circles and lines, angles, distances and areas --- rather like in Pythagoras's familiar theorem, but involving more geometric pieces, and more complex relations between them.) The hope is that the computer discovers and proves a statement that the human intellect finds striking and appealing, and yet is brand new: it had not been anticipated by geometers, nor can human mathematicians provide an alternative, perspicacious or easy proof.