Columbia Mathematics Department Colloquium

`On computer theorem-proving'


Carlos Simpson


We give an overview of what it means to use a computer proof verification
program. This can be compared with other related tools such as computer
algebra systems, and proof searchers. There are different approaches to
proof verification, coming from different philosophies of mathematics, and
these have an impact on the interface for mathematicians. We discuss why
proof verification is important to the development of all kinds of
mathematics, and what are the prospects for havinga useful system
in the near and medium future.

April 25th, Wednesday, 5:00-6:00 pm
Mathematics 520
Tea will be served at 4:30pm