[Alta-Logic] Computer Science Invited Speaker Wed 14:00

[Matthew Burke]

The following is an advertisement for a talk in the Computer Science Department.

Speaker: Jeremy Avigad

Time and Location: 14:00 Wed Mar 14th in ICT 616

Title: Formal Methods in Mathematics and the Lean Theorem Prover

Abstract: In computer science, the phrase "formal methods" is used to
describe a body of logic-based methods that are used to specify,
develop, and reason about hardware and software systems. These methods
can equally well be used to discover and verify mathematical claims,
however, and the boundary between mathematical and computational
applications is not a sharp one. In this talk, I will survey some of the
ways that formal methods have begun to make inroads in ordinary
mathematics, and some of the theoretical and practical challenges that
arise.

I will also discuss a new open-source theorem prover, Lean, which is
designed to support mathematical reasoning as well as hardware and
software verification. I will describe Lean's logical foundations and
some of the design decisions that were adopted to meet the challenges of
formal reasoning in mathematics.


http://peripatetic-seminar.cpsc.ucalgary.ca/wp/