Columbia
Mathematics Department
Colloquium
`On computer
theorem-proving'
by
Carlos Simpson
(CNRS-Nice)
Abstract:
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